gap (4r4p12-2) doc/make_doc

Summary

 doc/make_doc |    4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

    
download this patch

Patch contents

--- gap-4r4p12.orig/doc/make_doc
+++ gap-4r4p12/doc/make_doc
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 #W  make_doc						     Alexander Hulpke
 ##
 ##  This shell script constructs the (La)TeX .dvi, .ps, and .pdf formats and
@@ -53,4 +53,4 @@
 
 echo "Creating main manual HTML documentation (inc. comprehensive index)"
 # the main manuals + the comprehensive index
-(cd htm; make clean; make)
+#(cd htm; make clean; make)