On 15/10/2015 04:45, Ramana Kumar wrote:
I just realised I was _not_ on fixes-5.5.2 (although the SHA of the commit
I gave was correct).
So, the question is: why does master get this wrong?
A bug; now fixed. Thanks for letting me know.
Actually, I'm just wondering if configure should check for "git" and set
the start-up message to indicate the git commit number. That way it
would be clear whether it's master or a release version.
David
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
