From e9faaa3129f74c91313e5bbcf658d891bd351319 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 20 Apr 2018 10:24:01 +0200
Subject: Fix the script that generates the doc

---
 mathcomp/Makefile | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'mathcomp/Makefile')

diff --git a/mathcomp/Makefile b/mathcomp/Makefile
index e45d627..07f1869 100644
--- a/mathcomp/Makefile
+++ b/mathcomp/Makefile
@@ -23,7 +23,8 @@ MAKEFLAGS+=-B
 		-f Makefile.coq $* \
 		COQDEP='$(COQDEP) -exclude-dir plugin -c'
 
-clean:
+clean: 
+	$(H)[ -e Makefile.coq ] || $(call coqmakefile,ssreflect)
 	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
 		-f Makefile.coq clean
 	$(H)rm -f Makefile.coq
-- 
cgit v1.2.3