The configure file generate Make with a find

vbgl · Sep 25, 2014 · 58e57d7 · 58e57d7
1 parent d8a9e1c
commit 58e57d7
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 132 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,3 +1,4 @@
+Make
 Makefile
 Makefile.bak
 *.v.d

diff --git a/Make b/Make
diff --git a/Make.in b/Make.in
@@ -0,0 +1,4 @@
+# Library name
+-R . MathClasses
+
+# Coq files (filled by the configure)
diff --git a/configure.sh b/configure.sh
@@ -1,2 +1,4 @@
 #!/usr/bin/env sh
+cp -f Make.in Make
+find . -name "*.v" |grep -v misc/benchmarks_nobuild.v >>Make
 coq_makefile -f Make -o Makefile