summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorNadrieril2024-04-16 11:41:21 +0200
committerNadrieril2024-04-16 11:41:21 +0200
commit621b8fff5dcd8ad481fd151c8e0fea6e7438d070 (patch)
treea1c9dbb932960c94d4aadf54dd0bf6f7b6a5383d /Makefile
parent2545ad25384156d7d8d798567bc922be798a20e3 (diff)
Run sanity checks in CI only
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile3
1 files changed, 1 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 0f3e2999..0299d134 100644
--- a/Makefile
+++ b/Makefile
@@ -31,9 +31,8 @@ AENEAS_EXE ?= bin/aeneas
# The user can specify additional translation options for Aeneas.
# By default we activate the (expensive) sanity checks.
-OPTIONS ?= -checks
+OPTIONS ?=
-#
# The rules use (and update) the following variables
#
# The Charon test directory where to look for the .llbc files