]> matita.cs.unibo.it Git - helm.git/commitdiff
don't remove METAs on clean, but on distclean
authorStefano Zacchiroli <zack@upsilon.cc>
Sat, 24 Jan 2004 17:01:36 +0000 (17:01 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Sat, 24 Jan 2004 17:01:36 +0000 (17:01 +0000)
helm/hbugs/meta/Makefile

index 4d855ef54f33b24fa679ba1e5561f97ee81df870..af3f3f74bb810a84f8c27dc40ec2ab2e7170701e 100644 (file)
@@ -8,5 +8,5 @@ META.hbugs-thread-safe: META.hbugs-thread-safe.in
 META.hbugs-client: META.hbugs-client.in
        sed 's%@HBUGS_CLIENT_DIR@%$(CURDIR)/../client%' < $< > $@
 clean:
-       rm -f $(META)
 distclean: clean
+       rm -f $(META)