From 0ecec5c1512b5762f984c47ff07946ce63021d88 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 21 Jan 2015 09:37:05 +0100 Subject: [PATCH] `make devel` command, activating most flags, for developpers (see #27) --- Makefile | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index c397b0dd..d2288b04 100644 --- a/Makefile +++ b/Makefile @@ -125,7 +125,9 @@ update_next_tag: zsh -c 'sed -i "s/NEXT_VERSION/$(VERSION)/g" **/*.ml **/*.mli' zsh -c 'sed -i "s/NEXT_RELEASE/$(VERSION)/g" **/*.ml **/*.mli' -udpate_sequence: - git subtree pull --prefix sequence sequence stable --squash +devel: + ./configure --enable-bench --enable-tests --enable-misc \ + --enable-bigarray --enable-thread --enable-advanced + make all -.PHONY: examples push_doc tags qtest-gen qtest-clean update_sequence update_next_tag +.PHONY: examples push_doc tags qtest-gen qtest-clean devel update_next_tag