summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@google.com>2019-02-13 20:55:17 -0500
committerGravatar Benjamin Barenblat <bbaren@google.com>2019-02-17 16:45:25 -0500
commit8f33199e9e9342f1a0cbe3469fcfccf7f53cb4f2 (patch)
tree89787219aaefb883e45b49a81c0c71f3e2d1b089
parent9e7872b8a93a2f312f37d27c2290548e8b8a9424 (diff)
Make build verbose
-rwxr-xr-xdebian/rules3
1 files changed, 3 insertions, 0 deletions
diff --git a/debian/rules b/debian/rules
index e705617..48e004c 100755
--- a/debian/rules
+++ b/debian/rules
@@ -4,6 +4,9 @@
include /usr/share/coq/coqvars.mk
include /usr/share/ocaml/ocamlvars.mk
+# Show full commands when building.
+export VERBOSE := 1
+
ifeq ($(OCAML_NATDYNLINK),yes)
TARGET := opt
else