From 33fe2e6b28fe805e0452566cbfc7d70c5f3a0187 Mon Sep 17 00:00:00 2001 From: Bruno Guillaume <Bruno.Guillaume@loria.fr> Date: Wed, 10 Feb 2021 22:15:40 +0100 Subject: [PATCH] separated install_dev --- Makefile | 5 +---- _tags | 2 +- install_dev | 2 ++ 3 files changed, 4 insertions(+), 5 deletions(-) create mode 100755 install_dev diff --git a/Makefile b/Makefile index 2d80fb6..c337901 100644 --- a/Makefile +++ b/Makefile @@ -9,10 +9,7 @@ VERSION = `cat VERSION` default: native native: - $(OCB) grewpy.native - -byte: - $(OCB) grewpy.byte + $(OCB) -tag-line "true: package(libgrew)" grewpy.native install: native mkdir -p $(BINDIR) diff --git a/_tags b/_tags index 3cfcba8..b3a18d2 100644 --- a/_tags +++ b/_tags @@ -1,3 +1,3 @@ -true: package(yojson, threads, unix, str, containers, ANSITerminal, log, conll, amr, libgrew) +true: package(yojson, threads, unix, str, containers, ANSITerminal, log, conll, amr) true: thread true: bin_annot \ No newline at end of file diff --git a/install_dev b/install_dev new file mode 100755 index 0000000..d7c1b26 --- /dev/null +++ b/install_dev @@ -0,0 +1,2 @@ +ocamlbuild -use-ocamlfind -I src_ocaml -tag-line "true: package(libgrew_dev)" grewpy.native +cp grewpy.native ~/.local/bin/grewpy_dev -- GitLab