diff options
| author | Pierre-Marie Pédrot | 2019-10-03 17:08:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-03 17:08:56 +0200 |
| commit | ac54c19e1beca7663ae7742512d110a114ce9a62 (patch) | |
| tree | a96a05336c423ded9858e75fcdb96c2f150ade55 /Makefile.build | |
| parent | 3612ac1f639e361504cf3b2ded5609f5b643dfaa (diff) | |
| parent | b2c3eca7277ee9653e387ad3b599150b17c38572 (diff) | |
Merge PR #10765: Improved handling of micromega caches
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Ack-by: vbgl
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)) |