]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3551112) | patch
now should run also when the db is down (untested)
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 9 Sep 2004 16:36:46 +0000 (16:36 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 9 Sep 2004 16:36:46 +0000 (16:36 +0000)
commit017cd0cdd6a0bde85c25b230ffb8796d08ffc434
treef284511387b09d06ce608653d6eddee192f00b22tree | snapshot
parent35511123485cf133598fc447c55bc78a01678c6ecommit | diff
now should run also when the db is down (untested)
(the -nodb option is still unimplemented)
helm/gTopLevel/gTopLevel.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.