84a71d5259c2682403cdbd8710592410a2f128ab

The first line of this file holds the git revision number of the
last merge done from the master library sources.