From 9f1d62d6df01efad52608c82a2277942e3e50541 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <uni@thorsten-wissmann.de>
Date: Thu, 9 Jan 2014 12:46:21 +0100
Subject: [PATCH] Do not unnecessarily call make itself from make

This also makes the PARALLEL flag unnecessary. To do parallel build just
pass -j4 directly to make.
---
 Makefile | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/Makefile b/Makefile
index e648a1e..421995c 100644
--- a/Makefile
+++ b/Makefile
@@ -19,10 +19,6 @@ NATIVE := true
 # If defined, the dependencies will be updated automatically.
 CHECKDEP := 1
 
-# If defined, it indicates the number of cores
-# that make should use (e.g. -j2 for two cores).
-PARALLEL := -j2
-
 # The projects which will be compiled if "make all" is used.
 PROGS := coalg coalgcompare
 
@@ -59,8 +55,7 @@ LIBSMLI := $(patsubst %.mli,%.cmi,$(SOURCESMLI))
 LIBSML := $(patsubst %.ml,%$(SUFFIX),$(SOURCESML))
 
 .PHONY: all
-all:
-	$(MAKE) $(PARALLEL) $(PROGS)
+all: $(PROGS)
 
 minisat.cma: minisat.cmo minisat_stub.o
 	$(OCAMLC) -a -o minisat.cma minisat.cmo minisat_stub.o -custom -cclib -lminisat
-- 
GitLab