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 610af5fe40..f2e1ca4ea0 100644 --- a/Makefile.build +++ b/Makefile.build @@ -581,7 +581,7 @@ bin/votour.byte: $(VOTOURCMO) ########################################################################### CSDPCERTCMO:=clib/clib.cma $(addprefix plugins/micromega/, \ - mutils.cmo micromega.cmo \ + micromega.cmo mutils.cmo \ sos_types.cmo sos_lib.cmo sos.cmo csdpcert.cmo ) $(CSDPCERT): $(call bestobj, $(CSDPCERTCMO)) |