]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 024819e) | patch
1. metadata are no longer stored in .moo files.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 3 Dec 2005 10:35:10 +0000 (10:35 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 3 Dec 2005 10:35:10 +0000 (10:35 +0000)
commitdbb9f64a437b4abda0b9f47a527ab6135d596e28
tree92cea5fb5dd7862ae035e1f218297505f0309f27tree | snapshot
parent024819eeb7fcd370114ceb3dffc7907db92ab640commit | diff
1. metadata are no longer stored in .moo files.
   They are now stored (and retrieved) in .metadata files if -nodb is set.
   In this way the "library" library no longer depends on "content_pres"
2. removed files in grafite_parser that were commited by mistake
30 files changed:
helm/ocaml/METAS/meta.helm-grafite2.src diff | blob | history
helm/ocaml/METAS/meta.helm-library.src diff | blob | history
helm/ocaml/grafite/grafiteAst.ml diff | blob | history
helm/ocaml/grafite/grafiteAstPp.ml diff | blob | history
helm/ocaml/grafite/grafiteAstPp.mli diff | blob | history
helm/ocaml/grafite/grafiteMarshal.ml diff | blob | history
helm/ocaml/grafite/grafiteMarshal.mli diff | blob | history
helm/ocaml/grafite/grafiteParser.ml diff | blob | history
helm/ocaml/grafite2/grafiteEngine.ml diff | blob | history
helm/ocaml/grafite2/grafiteMisc.ml diff | blob | history
helm/ocaml/grafite2/grafiteMisc.mli diff | blob | history
helm/ocaml/grafite2/grafiteTypes.ml diff | blob | history
helm/ocaml/grafite2/grafiteTypes.mli diff | blob | history
helm/ocaml/grafite2/matitaSync.ml diff | blob | history
helm/ocaml/grafite_parser/grafiteDisambiguate.cmi [deleted file] blob | history
helm/ocaml/grafite_parser/grafiteDisambiguate.cmo [deleted file] blob | history
helm/ocaml/grafite_parser/grafiteDisambiguate.cmx [deleted file] blob | history
helm/ocaml/grafite_parser/grafiteDisambiguate.ml diff | blob | history
helm/ocaml/grafite_parser/grafiteDisambiguate.o [deleted file] blob | history
helm/ocaml/grafite_parser/grafite_parser.a [deleted file] blob | history
helm/ocaml/grafite_parser/grafite_parser.cma [deleted file] blob | history
helm/ocaml/grafite_parser/grafite_parser.cmxa [deleted file] blob | history
helm/ocaml/grafite_parser/matitaDisambiguator.cmx [deleted file] blob | history
helm/ocaml/library/.depend diff | blob | history
helm/ocaml/library/Makefile diff | blob | history
helm/ocaml/library/libraryClean.ml diff | blob | history
helm/ocaml/library/libraryMisc.ml diff | blob | history
helm/ocaml/library/libraryMisc.mli diff | blob | history
helm/ocaml/library/libraryNoDb.ml [new file with mode: 0644] blob
helm/ocaml/library/libraryNoDb.mli [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.