From 24bbb7712dca68e8fc9428ecba7062b87b3214e6 Mon Sep 17 00:00:00 2001
From: jjgarcia <jjgarcia>
Date: Sun, 9 Sep 2001 16:00:37 +0000
Subject: [PATCH] Avoid building BENCHMARK on all systems.

---
 src/doc/Makefile.in | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/doc/Makefile.in b/src/doc/Makefile.in
index e4c1f0239..d2c9e40a4 100644
--- a/src/doc/Makefile.in
+++ b/src/doc/Makefile.in
@@ -57,7 +57,7 @@ benchmark.html: $(srcdir)/benchmark.in.html ../gabriel/BENCHMARK
 	 echo '<pre>'; cat ../gabriel/BENCHMARK; echo '</pre>'; \
 	 cat $(srcdir)/end) | $(FILTER) > $@
 ../gabriel/BENCHMARK:
-	cd ../gabriel; make
+	echo '<b>Benchmark not available</b>' > ../gabriel/BENCHMARK
 license.html: $(top_srcdir)/../Copyright
 	(cat $(srcdir)/head; \
 	 echo '<pre>'; cat $?; echo '</pre>'; \