]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e66e67d) | patch
Bug fixed: the include_paths were no longer handled properly when matita was
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 8 Jan 2006 19:16:27 +0000 (19:16 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 8 Jan 2006 19:16:27 +0000 (19:16 +0000)
commit0767097b6f841f43d033b54b262e88423aef7da9
tree507fb5578532200aeaac15214191eb1b321aadcctree | snapshot
parente66e67d2f9f2772d63a7457e386f9616f62a2f39commit | diff
Bug fixed: the include_paths were no longer handled properly when matita was
launched outside a development. E.g.: ./matita library/nat/times.ma was no
longer working (./matita -I library library/nat/times.ma was)
helm/matita/matitaScript.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.