Sorry for the inconveniences.
On 04/17/2012 11:55 PM, Makarius wrote:
Here is another follow-up to the relcomp story so far:
changeset: 47508:85c6268b4071
tag: tip
user: wenzelm
date: Tue Apr 17 16:48:37 2012 +0200
files: doc-src/TutorialI/Sets/Relations.thy
description:
updated rel_comp ~> relcomp (cf. e1b761c216ac);
doc-src/TutorialI/Sets/Relations.thy
This is only to make the manual compile again.
This one didn't show up during 'isabelle makeall all'. Shouldn't
documentation be part of "all"? I guess then that a test should also
include "./Admin/build doc"? Anything else besides
isabelle makeall all
./Admin/build doc
to test a changeset (apart from external dependencies like the AFP)?
I hope it is not one of
the theories that need generated latex copied to another place by hand.
Just out of curiosity: what do you mean by the above statement?
Moreover NEWS in that version has oddities like this:
rel_comp_def ~> rel_comp_unfold
and later
rel_comp_unfold ~> relcomp_unfold
In the time immediately before the relase (which is now) the NEWS should
reflect the perspective for end-users of the official stable system that
is delivered.
I observed this oddities but left them deliberately since I was not
aware of the above convention (which is of course very sensible).
cheers
chris
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
