[isabelle] Annoying message about "unknown files"



Makarius,

you've introduced a warning for "isabelle build" that tells me when
files are not part of a Mercurial repository, like so:

### Unknown files (not part of a Mercurial repository):
###   /home/lars/work/reify/isabelle-cakeml/thy/generated/CakeML/Ast.thy
### ... many more lines ...

While this is technically correct – they're indeed not part of a
Mercurial repository –, it is also annoying, because they are part of a
Git repository.

Would it at least be possible to opt out of this warning? If I'm reading
the sources correctly, it is triggered by whether or not Isabelle itself
is under Mercurial control:

  check_unknown_files = Mercurial.is_repository(Path.explode("~~"))

That doesn't seem particularly useful to me. (The warning may be useful
to people who run stable Isabelle, for example.)

Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.