Dothem: no point not installing doc if we build it

It is the building part that is expensive.

diff --git a/Dothem b/Dothem
index c503a3767d57a869b26ed2eb6ffea60303c05c2e..deaf8fa9a60a23d6afea49381834a9533966602d 100755 (executable)
--- a/Dothem
+++ b/Dothem
@@ -92,16 +92,10 @@ do
                esac &&
 
                Meta/Make $M -- $J $dotest &&
-               case "$branch" in
-               jch)
-                       test -n "$nodoc" || Meta/Make $M -- doc install-doc
-                       ;;
-               master | maint | next )
-                       test -n "$nodoc" || Meta/Make $M -- doc
-                       ;;
-               *)
-                       : ;;
-               esac &&
+               {
+                       test -n "$nodoc" ||
+                       Meta/Make $M -- doc install-doc
+               } &&
                {
                        test z$install = znoinstall ||
                        Meta/Make $M -- install