From e224f7d4711b700b9e7583ba7452bc7587d1787c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 6 Jul 2005 13:53:19 +0000 Subject: [PATCH] clean did not remove matitatop* --- helm/matita/Makefile.in | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index c0c885433..009a6cec1 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -120,7 +120,8 @@ clean: matita matita.opt matitac matitac.opt \ cicbrowser cicbrowser.opt \ matitadep matitadep.opt \ - matitaclean matitaclean.opt + matitaclean matitaclean.opt \ + matitatop matitatop.opt distclean: clean rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli rm -f config.log config.status Makefile buildTimeConf.ml -- 2.39.2