]> matita.cs.unibo.it Git - helm.git/commit - helm/matita/dump_moo.ml
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dbb9f64) | patch
metadata are no longer stored in .moo files.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 3 Dec 2005 10:35:32 +0000 (10:35 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 3 Dec 2005 10:35:32 +0000 (10:35 +0000)
commit3ce38077e0b1e2a38ad513d3c108d7ef3c09bb7c
tree0b86e00690e3fcb1a3efd618386808b1439c0bactree | snapshot
parentdbb9f64a437b4abda0b9f47a527ab6135d596e28commit | diff
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"
helm/matita/dump_moo.ml diff | blob | history
helm/matita/matita.ml diff | blob | history
helm/matita/matitaEngine.ml diff | blob | history
helm/matita/matitaGui.ml diff | blob | history
helm/matita/matitacLib.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.