Dothem: Allow nodoc option

diff --git a/Dothem b/Dothem
index 7e2c5c2d97fb2971d2c7a69f2f0b58aea7aa1f38..9425b68c7d01a5fb919cf32a62307e9bff65623b 100755 (executable)
--- a/Dothem
+++ b/Dothem
@@ -4,12 +4,13 @@
 : ${BUILDBASE=../buildfarm}
 : ${branches='next master maint pu jch'}
 
-force= with_dash= M= install=
+force= with_dash= M= install= nodoc=
 while  case "$1" in
        -pedantic) M=$1 ;;
        -force) force=$1 ;;
        -dash) with_dash=y ;;
        -noinstall) install=noinstall ;;
+       -nodoc) nodoc=y ;;
        *) break ;;
        esac
 do
@@ -93,12 +94,12 @@ do
                Meta/Make $M -- $J all &&
                Meta/Make $M -- $J $dotest &&
                case "$branch" in
-               master | maint | next )
-                       Meta/Make $M -- doc
-                       ;;
-               jch )
+               jch)
                        Meta/Make $M -- doc install-doc
                        ;;
+               master | maint | next )
+                       test -z "$nodoc" || Meta/Make $M -- doc
+                       ;;
                *)
                        : ;;
                esac &&