On Sat, 24 Mar 2012, Ondřej Kunčar wrote:
The constant is now hidden.
Just two more things:
* "Now" means Isabelle/e64ffc96a49f -- The issue of proper references to
changesets is a running gag on isabelle-dev already. If you want, you can
make it the discriminating aspect between the two mailing lists:
isabelle-dev = proper hg ids, isabelle-users = some official release
(implicit). This does have a real practical impact, because old mail
threads are often studied later, e.g. 2 weeks or 2 months or 2 years. For
official releases the date stamp is sufficient, for continuous development
proper ids are required.
* The log entry for e64ffc96a49f is merely a rewording of the diff in
English prose, i.e. empty. There is an art of writing in half a sentence
what was done and why, to a give a hint to the one who needs to understand
things later (often many years). There is also a realistic danger of
fluctuation of small mishaps back and forth, if the history does not
explain the reasons.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
