aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-10-26 13:28:15 +0200
committerGaëtan Gilbert2018-10-26 13:28:15 +0200
commit3b14b406807af5503471d4936dea4d5ed0e0c789 (patch)
treecdbda0f6706c0b2be87cf32fb87b7e5551fffd25 /Makefile
parenta5854e84d083a6caf045d424ec34d47a9ffebcc4 (diff)
parent1db19a8f454e0f8c5a60101c87ccd38e0883d530 (diff)
Merge PR #8753: [build] Refactoring of config lib and ocamldebug tweaks.
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index b74e4e5d4f..9ac32625ab 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 dev/ocamldebug-coq dev/camlp5.dbg config/Info-*.plist
+ rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq config/Info-*.plist
distclean: clean cleanconfig cacheclean timingclean