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 0dda6140cf..b68a02cf64 100644 --- a/Makefile.build +++ b/Makefile.build @@ -68,7 +68,7 @@ ALLDEPS:=$(addsuffix .d, \ VERBOSE= NO_RECOMPILE_ML4= NO_RECALC_DEPS= -READABLE_ML4=1 # non-empty means .ml of .ml4 will be ascii instead of binary +READABLE_ML4= # 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" |