From bc20368fc207592688ebb526e3fa427ec4af3286 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 7 Nov 2019 13:47:34 +0100
Subject: [PATCH] Don't re-generate _CoqProject in create_makefile.sh
No need to re-generate an unchanging file from scratch.
---
.gitignore | 1 -
_CoqProject | 1 +
create_makefile.sh | 4 ----
3 files changed, 1 insertion(+), 5 deletions(-)
create mode 100644 _CoqProject
diff --git a/.gitignore b/.gitignore
index 4b9c49399..4ec65516f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -5,7 +5,6 @@
/html
*.aux
Makefile*
-_CoqProject
*.crashcoqide
*.v#
*.cache
diff --git a/_CoqProject b/_CoqProject
new file mode 100644
index 000000000..8cc374e63
--- /dev/null
+++ b/_CoqProject
@@ -0,0 +1 @@
+-R . rt -arg "-w -notation-overriden,-parsing"
diff --git a/create_makefile.sh b/create_makefile.sh
index 46c35de0c..876be759a 100755
--- a/create_makefile.sh
+++ b/create_makefile.sh
@@ -14,10 +14,6 @@ do
shift
done
-# Include rt-proofs library in _CoqProject.
-# (For Coq versions >= 8.6, remove spurious warnings.)
-echo -R . rt -arg \"-w -notation-overriden,-parsing\" > _CoqProject
-
# Compile all *.v files
if [ "yes" == "$SKIP_CLASSIC" ]
then
--
GitLab