diff options
-rw-r--r-- | round-robin.sh | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/round-robin.sh b/round-robin.sh index 5015c716..f6bc2445 100644 --- a/round-robin.sh +++ b/round-robin.sh @@ -205,6 +205,14 @@ EOF chmod +x "$(pwd)/bin/g++" cp "$(pwd)/bin/g++" "$(pwd)/bin/c++" + # Disable building documention. Apparently, this is one of + # the most popular ways. + cat > "$(pwd)/bin/makeinfo" <<EOF +#!/bin/sh +exec true +EOF + chmod +x "$(pwd)/bin/makeinfo" + PATH=$(pwd)/bin:$PATH export PATH @@ -398,6 +406,7 @@ build_abe () $action \ $target_opt \ --extraconfigdir config/master \ + --disable make_docs \ $custom_abe_src_opt \ $stage & res=0 && wait $! || res=$? |