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 8d1f3f4f..0bf2d3eb 100644 --- a/Makefile.build +++ b/Makefile.build @@ -262,7 +262,7 @@ endef CAMLP5DEPS:=grammar/grammar.cma CAMLP5USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) -PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) +PR_O := $(if $(READABLE_ML4),pr_o.cmo,) # Main packages linked by Coq. SYSMOD:=-package num,str,unix,dynlink,threads |