From 607503b28fca50f4b76b2237d5ca13802b8252fa Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Fri, 12 Dec 2014 18:01:16 +0100 Subject: #4843 part 2 : The .cmxs files for plug-ins must have execute permission --- Makefile.build | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile.build b/Makefile.build index c4fc69a59..52f67dc8e 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 -- cgit v1.2.3