a5bfd9da1d1b24f326399b6b75558ded14514f23

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