aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index a15870faca..b74e4e5d4f 100644
--- a/Makefile
+++ b/Makefile
@@ -261,7 +261,7 @@ cacheclean:
find theories plugins test-suite -name '.*.aux' -exec rm -f {} +
cleanconfig:
- rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp5.dbg config/Info-*.plist
+ rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq dev/camlp5.dbg config/Info-*.plist
distclean: clean cleanconfig cacheclean timingclean