diff options
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common index 654a715272..8fa2e5b766 100644 --- a/Makefile.common +++ b/Makefile.common @@ -81,7 +81,7 @@ SRCDIRS:=\ # Order is relevent here because kernel and checker contain files # with the same name -CHKSRCDIRS:= checker lib config kernel +CHKSRCDIRS:= checker lib config kernel parsing ########################################################################### # tools @@ -225,7 +225,7 @@ IDEMOD:=$(shell cat ide/ide.mllib) # coqmktop, coqc COQENVCMO:=lib/clib.cma\ - lib/pp_control.cmo lib/compat.cmo lib/pp.cmo lib/loc.cmo lib/errors.cmo + lib/loc.cmo lib/errors.cmo COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo |