f9ea41683444ebe11cfa45b05223899764df28fb

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