matita.cs.unibo.it Git - helm.git/commit - matita/matita/matitaGui.ml

]> matita.cs.unibo.it Git - helm.git/commit - matita/matita/matitaGui.ml

author	Andrea Asperti <andrea.asperti@unibo.it>
	Fri, 5 Nov 2010 15:18:53 +0000 (15:18 +0000)
committer	Andrea Asperti <andrea.asperti@unibo.it>
	Fri, 5 Nov 2010 15:18:53 +0000 (15:18 +0000)
commit	d8c17db3c787f3ea964bbcd3b27427ca44b356d0
tree	fd941f5d5f865ba75c2ee6f8507a5bd1042aa91f	tree \| snapshot
parent	098e3728bb1d993145b893b83ac6e01173b58486	commit \| diff

Huge change!!!

- matitadep & co removed (RIP)
- both matita and matitac can now recursively compile files as needed
- librarian greatly simplified: now it only handles roots

Probably many bugs left.

20 files changed:

matita/components/grafite_engine/grafiteEngine.ml		diff \| blob \| history
matita/components/grafite_engine/grafiteTypes.ml		diff \| blob \| history
matita/components/grafite_engine/grafiteTypes.mli		diff \| blob \| history
matita/components/grafite_parser/Makefile		diff \| blob \| history
matita/components/grafite_parser/dependenciesParser.ml	[deleted file]	blob \| history
matita/components/grafite_parser/dependenciesParser.mli	[deleted file]	blob \| history
matita/components/library/librarian.ml		diff \| blob \| history
matita/components/library/librarian.mli		diff \| blob \| history
matita/components/ng_library/nCicLibrary.ml		diff \| blob \| history
matita/components/ng_library/nCicLibrary.mli		diff \| blob \| history
matita/components/statuses.txt		diff \| blob \| history
matita/matita/Makefile		diff \| blob \| history
matita/matita/matitaEngine.ml		diff \| blob \| history
matita/matita/matitaEngine.mli		diff \| blob \| history
matita/matita/matitaExcPp.ml		diff \| blob \| history
matita/matita/matitaGui.ml		diff \| blob \| history
matita/matita/matitaScript.ml		diff \| blob \| history
matita/matita/matitac.ml		diff \| blob \| history
matita/matita/matitadep.ml	[deleted file]	blob \| history
matita/matita/matitadep.mli	[deleted file]	blob \| history

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom