]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9ca6b45) | patch
avoid deletion of useful .cmi with .PRECIOUS
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 4 Sep 2003 16:45:44 +0000 (16:45 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 4 Sep 2003 16:45:44 +0000 (16:45 +0000)
commit811c9c106279d504c214b54a267b62653d685945
tree3625813be386432136a2ec8ec99f3ccd7e55d18dtree | snapshot
parent9ca6b45a45f1cc4cb30a4f36f9939dbedf657e6ecommit | diff
avoid deletion of useful .cmi with .PRECIOUS
helm/hbugs/tutors/Makefile diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.