Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
POTTIER Francois
menhir
Commits
1e34d32c
Commit
1e34d32c
authored
Oct 20, 2015
by
POTTIER Francois
Browse files
Added [make local] for local installation of the development version.
parent
90b68214
Changes
1
Hide whitespace changes
Inline
Side-by-side
GNUmakefile
View file @
1e34d32c
...
...
@@ -6,7 +6,7 @@
SHELL
:=
bash
.PHONY
:
all test clean package check export godi opam
.PHONY
:
all test clean package check export godi opam
local
# -------------------------------------------------------------------------
...
...
@@ -253,3 +253,12 @@ opam:
@ echo "If happy, please run
:
"
@
echo
" cd
$(OPAM)
/packages/menhir && git commit -a && git push && firefox https://github.com/"
@
echo
"and issue a pull request."
# -------------------------------------------------------------------------
# Re-installing locally. This can overwrite an existing local installation.
local
:
$(MAKE)
package
$(MAKE)
-C
$(PACKAGE)
PREFIX
=
/usr/local
USE_OCAMLFIND
=
false
all
sudo
$(MAKE)
-C
$(PACKAGE)
PREFIX
=
/usr/local
USE_OCAMLFIND
=
false install
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment