From 86b7efbdbe3c2da0f788df3ee7839cf3b88f7120 Mon Sep 17 00:00:00 2001
From: Eelco Dolstra <e.dolstra@tudelft.nl>
Date: Mon, 16 Feb 2004 16:48:06 +0000
Subject: [PATCH] * Don't build ATerm library if we don't need to.

---
 externals/Makefile.am | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/externals/Makefile.am b/externals/Makefile.am
index 4819b95fe..6da79ab8a 100644
--- a/externals/Makefile.am
+++ b/externals/Makefile.am
@@ -50,6 +50,9 @@ have-aterm:
 	$(MAKE) $(ATERM)
 	touch have-aterm
 
+if HAVE_ATERM
+build-aterm:
+else
 build-aterm: have-aterm
 	(pfx=`pwd` && \
 	cd $(ATERM) && \
@@ -58,6 +61,7 @@ build-aterm: have-aterm
 	make && \
 	make install)
 	touch build-aterm
+endif
 
 
 all: build-db build-aterm