diff options
| author | Frédéric Besson | 2019-09-17 18:09:06 +0200 |
|---|---|---|
| committer | Frédéric Besson | 2019-10-03 14:31:13 +0200 |
| commit | 65b89a6b06b5ff2e26883800702cda19d2d980df (patch) | |
| tree | 1c740c10f52d7ad08eb448eb093e42c0510f7c95 /Makefile.build | |
| parent | 92a55bf800a34b5ec283ce0419cde98f3312c9b8 (diff) | |
Improved handling of micromega caches
- Specialised hash and equality functions.
Avoid collisions in extreme scenarios.
- Flags to disable the use of the caches.
fixes #10772
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)) |