From fd204b20e4ac3c41e1826f99344023d294a834c0 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 26 Feb 2015 23:52:05 +0100 Subject: Removed the glob files from doc/ instead of doc/glob/ --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 3a684743..6fd8d2a6 100644 --- a/Makefile +++ b/Makefile @@ -182,7 +182,7 @@ latexdoc: cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES) %.vo: %.v - @rm -f doc/glob/$(*F).glob + @rm -f doc/$(*F).glob @echo "COQC $*.v" @$(COQC) -dump-glob doc/$(*F).glob $*.v -- cgit