aboutsummaryrefslogtreecommitdiff
path: root/Makefile.make
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-20 22:02:10 +0000
committerGitHub2020-11-20 22:02:10 +0000
commit5b15fce17d856dfbd51482f724ddf5e5f9646073 (patch)
treee42bea1a6427ad941ebc4c70cf568e8f81f90007 /Makefile.make
parent23d30fa1c19af9a29787204d81d7bd2d2e0c9b1f (diff)
parent76ab524320e3d4c006c6c94372e0cfda2b62c76e (diff)
Merge PR #13248: Build all_stdlib.v in test suite makefile
Reviewed-by: ejgallego
Diffstat (limited to 'Makefile.make')
-rw-r--r--Makefile.make1
1 files changed, 0 insertions, 1 deletions
diff --git a/Makefile.make b/Makefile.make
index 34f5707ae8..2f6781439c 100644
--- a/Makefile.make
+++ b/Makefile.make
@@ -253,7 +253,6 @@ docclean:
archclean: clean-ide optclean voclean plugin-tutorialclean
rm -rf _build _build_boot
- rm -f $(ALLSTDLIB).*
optclean:
rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBINOPT)