diff --git a/src/doc/Makefile.in b/src/doc/Makefile.in index d2c9e40a4..1749a1515 100644 --- a/src/doc/Makefile.in +++ b/src/doc/Makefile.in @@ -57,7 +57,9 @@ benchmark.html: $(srcdir)/benchmark.in.html ../gabriel/BENCHMARK echo '
'; cat ../gabriel/BENCHMARK; echo '
'; \ cat $(srcdir)/end) | $(FILTER) > $@ ../gabriel/BENCHMARK: - echo 'Benchmark not available' > ../gabriel/BENCHMARK + cd ../gabriel; \ + if (which lisp && which clisp) > /dev/null; then make; \ + else \ echo "No benchmarks available" > BENCHMARK; fi license.html: $(top_srcdir)/../Copyright (cat $(srcdir)/head; \ echo '
'; cat $?; echo '
'; \