diff options
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.common b/Makefile.common index efc3bb7ef..8f6e1b808 100644 --- a/Makefile.common +++ b/Makefile.common @@ -37,6 +37,7 @@ endif INSTALLBIN:=install INSTALLLIB:=install -m 644 +INSTALLSH:=./install.sh MKDIR:=install -d COQIDEBYTE:=bin/coqide.byte$(EXE) |