Dear all,
to update the change history of one of my AFP entries, I ran
admin/sitegen. I noticed that as a result some other sites changed too.
All the changes where along the lines of
-(revision <a
href="http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/f74a8be156a7";>f74a8be156a7</a>)<br>
+(revision f74a8be156a7)<br>
in corresponding *.shtml files, i.e., links to changesets are replaced
by the mere short-form changeset ID. Is this on purpose or did I do
something wrong? (I will of course refrain from pushing any changes
until I got an answer.)
cheers
chris
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
