On Fri, 14 Dec 2012, Johannes Hölzl wrote: >> Anythying that needs to be added to Admin/Mercurial/Central/README can be >> discussed here (or privately). > > I think we should add the trick by Alex to use strip. I have add some more text in Isabelle/325bf9073c59. Makarius