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 3aa681bfd..bd236682e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -771,7 +771,7 @@ ifndef CUSTOM endif ifeq ($(BEST),opt) $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) - $(INSTALLBIN) $(FULLCOQLIB) $(PLUGINSOPT) + $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT) endif # csdpcert is not meant to be directly called by the user; we install # it with libraries |