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