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 a0461d7a3..2ccf0ee86 100644 --- a/Makefile.build +++ b/Makefile.build @@ -663,7 +663,7 @@ endif # csdpcert is not meant to be directly called by the user; # we install it with libraries -$(MKDIR) -p $(FULLCOQLIB)/contrib/micromega - $(INSTALLBIN) $(CDSPCERT) $(FULLCOQLIB)/contrib/micromega + $(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/contrib/micromega install-library-light: $(MKDIR) $(FULLCOQLIB) |