]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5433a13) | patch
- added support for "-nodb" flag (still missing support for matitaclean which relies...
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 5 Oct 2005 09:12:23 +0000 (09:12 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 5 Oct 2005 09:12:23 +0000 (09:12 +0000)
commitafe21e48aefe81db3ca150fac9a5bbfbc893fa59
tree6b418d2f0f5fe715a4e5f541fc2562ab65b6f157tree | snapshot
parent5433a131a7ff29529747e58c68dbf258d696e55bcommit | diff
- added support for "-nodb" flag (still missing support for matitaclean which relies on the db)
- centralized parsing of cmdline options in matitaInit. All top level programs which need to parse cmdline will now invoke either MatitaInit.parse_cmdline or MatitaInit.initialize_all and then refer to the relevant keys in the registry
- changed dependencies on hMySql since now it is in a separate library
12 files changed:
helm/matita/Makefile.in diff | blob | history
helm/matita/configure.ac diff | blob | history
helm/matita/matita.ml diff | blob | history
helm/matita/matitaGui.ml diff | blob | history
helm/matita/matitaInit.ml diff | blob | history
helm/matita/matitaInit.mli diff | blob | history
helm/matita/matitaMathView.ml diff | blob | history
helm/matita/matitacLib.ml diff | blob | history
helm/matita/matitaclean.ml diff | blob | history
helm/matita/matitacleanLib.ml diff | blob | history
helm/matita/matitadep.ml diff | blob | history
helm/matita/matitamake.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.