diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index db2d0f720..6d12063ca 100644 --- a/Makefile.build +++ b/Makefile.build @@ -59,7 +59,7 @@ CURDEPS:=$(addsuffix .d, $(CURFILES)) VERBOSE= NO_RECOMPILE_ML4= NO_RECALC_DEPS= -READABLE_ML4= # non-empty means .ml of .ml4 will be ascii instead of binary +READABLE_ML4=true # non-empty means .ml of .ml4 will be ascii instead of binary VALIDATE= COQ_XML= # is "-xml" when building XML library VM= # is "-no-vm" to not use the vm" |