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