From 76ab524320e3d4c006c6c94372e0cfda2b62c76e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 22 Oct 2020 15:30:30 +0200
Subject: Build all_stdlib.v in test suite makefile

instead of recursive make
---
 Makefile.make | 1 -
 1 file changed, 1 deletion(-)

(limited to 'Makefile.make')

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)
-- 
cgit v1.2.3