From 7f462118e02e539b43b99c2ef96363c166d953bf Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Fri, 15 Jul 2016 13:51:26 +0200
Subject: [PATCH] Fix create_makefile on Windows (MSYS2 shell)

---
 Makefile           |  2 +-
 create_makefile.sh | 12 +++---------
 2 files changed, 4 insertions(+), 10 deletions(-)

diff --git a/Makefile b/Makefile
index 945365dae..0fb66166a 100644
--- a/Makefile
+++ b/Makefile
@@ -65,7 +65,7 @@ OPT?=
 COQDEP?="$(COQBIN)coqdep" -c
 COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
 COQCHKFLAGS?=-silent -o
-COQDOCFLAGS?=-interpolate -utf8 --parse-comments --external https://math-comp.github.io/math-comp/htmldoc/ mathcomp
+COQDOCFLAGS?=-interpolate -utf8 --plain-comments --parse-comments --external https://math-comp.github.io/math-comp/htmldoc/ mathcomp
 COQC?=$(TIMER) "$(COQBIN)coqc"
 GALLINA?="$(COQBIN)gallina"
 COQDOC?="$(COQBIN)coqdoc"
diff --git a/create_makefile.sh b/create_makefile.sh
index fdd0fbe0f..89c3e0560 100755
--- a/create_makefile.sh
+++ b/create_makefile.sh
@@ -7,28 +7,22 @@ coq_makefile -f _CoqProject $(find . -name "*.v" ! -name "*#*" ! -name "*eqdec*.
 # adds the rt. prefix
 if [ "$(uname)" == "Darwin" ]; then
 	sed -i '' 's|$(notdir $(^:.vo=))|$(addprefix rt., $(subst /,., $(^:.vo=)))|g' Makefile
-elif [ "$(expr substr $(uname -s) 1 5)" == "Linux" ]; then
+else
 	sed -i 's|$(notdir $(^:.vo=))|$(addprefix rt., $(subst /,., $(^:.vo=)))|g' Makefile
-elif [ "$(expr substr $(uname -s) 1 10)" == "MINGW32_NT" ]; then
-	:
 fi
 
 
 # Fix 'make html' so that it parses comments and has links to ssreflect.
 if [ "$(uname)" == "Darwin" ]; then
 	sed -i '' 's|-interpolate -utf8|-interpolate -utf8 --plain-comments --parse-comments --external https://math-comp.github.io/math-comp/htmldoc/ mathcomp|g' Makefile
-elif [ "$(expr substr $(uname -s) 1 5)" == "Linux" ]; then
+else
 	sed -i 's|-interpolate -utf8|-interpolate -utf8 --plain-comments --parse-comments --external https://math-comp.github.io/math-comp/htmldoc/ mathcomp|g' Makefile
-elif [ "$(expr substr $(uname -s) 1 10)" == "MINGW32_NT" ]; then
-	:
 fi
 
 # Fix 'make clean' to remove all binary files, regardless of name
 if [ "$(uname)" == "Darwin" ]; then
 	sed -i '' 's|rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)|find . -name "*.vo" -delete -o -name "*.glob" -delete -o -name "*.v.d" -delete -o -name "*.vio" -delete -o -name "*.old" -delete -o -name "*.beautified" -delete|g' Makefile
-elif [ "$(expr substr $(uname -s) 1 5)" == "Linux" ]; then
+else
 	sed -i 's|rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)|find . -name "*.vo" -delete -o -name "*.glob" -delete -o -name "*.v.d" -delete -o -name "*.vio" -delete -o -name "*.old" -delete -o -name "*.beautified" -delete|g' Makefile
-elif [ "$(expr substr $(uname -s) 1 10)" == "MINGW32_NT" ]; then
-	:
 fi
 
-- 
GitLab