diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rwxr-xr-x | install.sh | 7 |
2 files changed, 7 insertions, 2 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 diff --git a/install.sh b/install.sh index 4b3abe5c6..c5835b014 100755 --- a/install.sh +++ b/install.sh @@ -7,5 +7,10 @@ for f; do bn=`basename $f` dn=`dirname $f` install -d "$dest/$dn" - install -m 644 $f "$dest/$dn/$bn" + case $bn in + *.cmxs) install -m 755 $f "$dest/$dn/$bn" + ;; + *) install -m 644 $f "$dest/$dn/$bn" + ;; + esac done |