summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 4dc1475b..0fc3fcf4 100644
--- a/Makefile
+++ b/Makefile
@@ -48,7 +48,7 @@ trans-hashmap_main: SUBDIR:=hashmap_on_disk
trans-nll-betree_nll: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
trans-nll-betree_nll: SUBDIR:=misc
-trans-constants: TRANS_OPTIONS += -no-split-files -no-state -no-decreases-clauses
+trans-constants: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
trans-constants: SUBDIR:=misc
trans-external: TRANS_OPTIONS +=