diff options
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index ccf79331d8..1a6424c950 100644 --- a/Makefile.common +++ b/Makefile.common @@ -255,7 +255,8 @@ PARSERREQUIRESCMX:=$(LINKCMX) $(PARSERCMA:.cma=.cmxa) CSDPCERTCMO:=$(addprefix plugins/micromega/, \ mutils.cmo micromega.cmo mfourier.cmo certificate.cmo \ - sos.cmo csdpcert.cmo ) + sos_types.cmo sos_lib.cmo sos.cmo csdpcert.cmo ) + CSDPCERTCMX:= $(CSDPCERTCMO:.cmo=.cmx) DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma |