diff options
| author | Pierre Boutillier | 2014-12-12 18:01:16 +0100 |
|---|---|---|
| committer | Pierre Boutillier | 2014-12-12 18:02:30 +0100 |
| commit | 607503b28fca50f4b76b2237d5ca13802b8252fa (patch) | |
| tree | 2d4cd9d4ddee1fade35728949daa8b67ca0da89e | |
| parent | a8169a718ca48070d4d5bce71fd302ff6148b8f0 (diff) | |
#4843 part 2 : The .cmxs files for plug-ins must have execute permission
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index c4fc69a59f..52f67dc8e2 100644 --- a/Makefile.build +++ b/Makefile.build @@ -769,7 +769,7 @@ ifndef CUSTOM endif ifeq ($(BEST),opt) $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT) + $(INSTALLBIN) $(FULLCOQLIB) $(PLUGINSOPT) endif # csdpcert is not meant to be directly called by the user; we install # it with libraries |