From ac5ccfe03b4a79273bc71654880ce94286d70f74 Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Thu, 14 Jul 2016 15:45:51 +0200
Subject: [PATCH] Fix create_makefile script to work on Mac and Linux

---
 create_makefile.sh | 28 ++++++++++++++++++++++++----
 1 file changed, 24 insertions(+), 4 deletions(-)

diff --git a/create_makefile.sh b/create_makefile.sh
index a064565ae..fdd0fbe0f 100755
--- a/create_makefile.sh
+++ b/create_makefile.sh
@@ -1,14 +1,34 @@
 # Compile all *.v files (except the ones that define the decidable equality). Those
 # are directly included in other files.
-coq_makefile -f _CoqProject $(find -name "*.v" ! -name "*#*" ! -name "*eqdec*.v" -print) -o Makefile
+coq_makefile -f _CoqProject $(find . -name "*.v" ! -name "*#*" ! -name "*eqdec*.v" -print) -o Makefile
 
 # Fix the 'make validate' command. It doesn't handle the library prefix properly
 # and cause clashes for files with the same name. This forces full filenames and
 # adds the rt. prefix
-sed -i 's|$(notdir $(^:.vo=))|$(addprefix rt., $(subst /,., $(^:.vo=)))|g' Makefile
+if [ "$(uname)" == "Darwin" ]; then
+	sed -i '' 's|$(notdir $(^:.vo=))|$(addprefix rt., $(subst /,., $(^:.vo=)))|g' Makefile
+elif [ "$(expr substr $(uname -s) 1 5)" == "Linux" ]; then
+	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.
-sed -i 's|-interpolate -utf8|-interpolate -utf8 --parse-comments --external https://math-comp.github.io/math-comp/htmldoc/ mathcomp|g' Makefile
+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
+	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
-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
+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
+	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