]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d922e60) | patch
An object should be removed from disk (i.e. from the Getter scope) _before_ removing it
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 22 Jul 2005 14:33:53 +0000 (14:33 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 22 Jul 2005 14:33:53 +0000 (14:33 +0000)
commit6d9f41964a95bc6fe6d9e7d47331ac7f8574fd17
treec70dc1cf37e00b8d060c0d393f42af340c28ca74tree | snapshot
parentd922e6065ae8adadf09afbce0f3b2abe72b5bc1ccommit | diff
An object should be removed from disk (i.e. from the Getter scope) _before_ removing it
from the environment.
helm/matita/matitacleanLib.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.