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