[isabelle-dev] Incomplete .hgignore?

Tjark Weber webertj at in.tum.de
Tue Aug 14 15:27:24 CEST 2012


Hi,

Building the repository version (7476665f3e0f) with "isabelle build -a"
generates a number of files that Mercurial doesn't know about (see
below). I could simply add them to .hgignore, but perhaps someone who
knows why these files are generated would be more qualified to do so?

Best regards,
Tjark

$ bin/isabelle build -a
[...]
$ hg status
? doc-src/Classes/Thy/document/Code_Integer.tex
? doc-src/Classes/Thy/document/Code_Natural.tex
? doc-src/Classes/Thy/document/Setup.tex
? doc-src/Classes/Thy/document/session.tex
? doc-src/Codegen/Thy/document/Setup.tex
? doc-src/Codegen/Thy/document/session.tex
? doc-src/Codegen/Thy/examples/rat.ML
? doc-src/Functions/Thy/document/session.tex
? doc-src/IsarImplementation/Thy/document/session.tex
? doc-src/IsarRef/Thy/document/Base.tex
? doc-src/IsarRef/Thy/document/Old_Recdef.tex
? doc-src/IsarRef/Thy/document/Wfrec.tex
? doc-src/IsarRef/Thy/document/session.tex
? doc-src/LaTeXsugar/Sugar/document/session.tex
? doc-src/Main/Docs/document/session.tex
? doc-src/ProgProve/Thys/document/MyList.tex
? doc-src/ProgProve/Thys/document/session.tex
? doc-src/System/Thy/document/session.tex
? doc-src/TutorialI/document/Basic.tex
? doc-src/TutorialI/document/Binomial.tex
? doc-src/TutorialI/document/Blast.tex
? doc-src/TutorialI/document/Examples.tex
? doc-src/TutorialI/document/Force.tex
? doc-src/TutorialI/document/Forward.tex
? doc-src/TutorialI/document/Functions.tex
? doc-src/TutorialI/document/Primes.tex
? doc-src/TutorialI/document/Recur.tex
? doc-src/TutorialI/document/Relations.tex
? doc-src/TutorialI/document/Setup.tex
? doc-src/TutorialI/document/Tacticals.tex
? doc-src/TutorialI/document/session.tex
? doc-src/ZF/document/FOL_examples.tex
? doc-src/ZF/document/IFOL_examples.tex
? doc-src/ZF/document/If.tex
? doc-src/ZF/document/ZF_examples.tex
? doc-src/ZF/document/session.tex
? src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.prv
? src/HOL/SPARK/Examples/Liseq/liseq/liseq_length.prv
? src/HOL/SPARK/Examples/RIPEMD-160/rmd/f.prv
? src/HOL/SPARK/Examples/RIPEMD-160/rmd/hash.prv
? src/HOL/SPARK/Examples/RIPEMD-160/rmd/k_l.prv
? src/HOL/SPARK/Examples/RIPEMD-160/rmd/k_r.prv
? src/HOL/SPARK/Examples/RIPEMD-160/rmd/r_l.prv
? src/HOL/SPARK/Examples/RIPEMD-160/rmd/r_r.prv
? src/HOL/SPARK/Examples/RIPEMD-160/rmd/round.prv
? src/HOL/SPARK/Examples/RIPEMD-160/rmd/s_l.prv
? src/HOL/SPARK/Examples/RIPEMD-160/rmd/s_r.prv
? src/HOL/SPARK/Examples/Sqrt/sqrt/isqrt.prv
? src/HOL/SPARK/Manual/complex_types_app/initialize.prv
? src/HOL/SPARK/Manual/loop_invariant/proc1.prv
? src/HOL/SPARK/Manual/loop_invariant/proc2.prv
? src/HOL/SPARK/Manual/simple_greatest_common_divisor/g_c_d.prv

-- 
Ceterum censeo: Isabelle needs an issue tracker.



More information about the isabelle-dev mailing list