From aa28542959e52443494cd8e72eb99b00b28f8791 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 11 Aug 2015 20:34:23 +0200 Subject: [PATCH] update makefile (target devel) --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 81d3621b..f9c35b2a 100644 --- a/Makefile +++ b/Makefile @@ -143,7 +143,7 @@ update_next_tag: zsh -c 'sed -i "s/NEXT_RELEASE/$(VERSION)/g" **/*.ml **/*.mli' devel: - ./configure --enable-bench --enable-tests --enable-misc \ + ./configure --enable-bench --enable-tests --enable-misc --enable-unix \ --enable-bigarray --enable-thread --enable-advanced make all