From 0c06c06d7ba9cdcfacdeb4d239a78b4cefb97b62 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Tue, 8 Sep 2020 10:13:06 -0500
Subject: [PATCH] Document Makefile flags together

---
 CONTRIBUTING.md    | 2 ++
 Makefile.coq.local | 6 ++++++
 2 files changed, 8 insertions(+)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index c8d4924bf..67eef817f 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -46,6 +46,8 @@ Some test cases have per-Coq-version `.ref` files (e.g., `atomic.8.8.ref` is a
 Coq-8.8-specific `.ref` file).  If you change one of these, remember to update
 *all* the `.ref` files.
 
+If you want to compile without tests run `make NO_TEST=1`.
+
 ## How to measure the timing effect on a reverse dependency
 
 So say you did a change in Iris, and want to know how it affects [lambda-rust]
diff --git a/Makefile.coq.local b/Makefile.coq.local
index 9ceafe4c7..d9758f033 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -1,3 +1,9 @@
+# use NO_TEST=1 to skip the tests
+NO_TEST:=
+
+# use MAKE_REF=1 to generate new reference files
+MAKE_REF:=
+
 # Run tests interleaved with main build.  They have to be in the same target for this.
 real-all: $(if $(NO_TEST),,test)
 
-- 
GitLab