diff options
Diffstat (limited to '')
| -rw-r--r-- | Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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 += |