]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b67ea51) | patch
do not delete Makefile and Makefile.common on distclean since they are no
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 3 Feb 2006 15:19:37 +0000 (15:19 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 3 Feb 2006 15:19:37 +0000 (15:19 +0000)
commitcf59c0f6b6e082b49caaf7ba3745e08b1a845be5
treeef3db4347f18564a02411b3831b1140ef6e214a4tree | snapshot
parentb67ea513f11d1ef3d9fd228c64913561424662e2commit | diff
do not delete Makefile and Makefile.common on distclean since they are no
longer generated at configure time
helm/ocaml/Makefile diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.