summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
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