]> matita.cs.unibo.it Git - helm.git/commit
MATITA_* env variable preserved when publishing a development
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 23 May 2007 14:08:27 +0000 (14:08 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 23 May 2007 14:08:27 +0000 (14:08 +0000)
commit105a6097411efd3ab1a198426dcf30d9943013e3
tree95f1210f2b491dcdafb92c30981974a7ffe89e94
parent9da16ebf1736b345ef6f3c4d9e0c107ed049ba4e
MATITA_* env variable preserved when publishing a development
helm/software/matita/matitamakeLib.ml