diff options
| author | Pierre Boutillier | 2014-12-17 11:11:43 +0100 |
|---|---|---|
| committer | Pierre Boutillier | 2014-12-17 11:56:15 +0100 |
| commit | c854f859115add2ed95e2e4df36bce2eb2e6f22a (patch) | |
| tree | 8db8ed8068064a3369b3fe20bdcac35d24e05b9a /Makefile.build | |
| parent | a65f9028c4834fe2ae803d1155780c1caf6790c4 (diff) | |
Revert and correctly fix "#4843 part 2 : The .cmxs files for plugins must have x permission"
This reverts commit 607503b28fca50f4b76b2237d5ca13802b8252fa.
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 3aa681bfde..bd236682ee 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 |