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