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