From f6d7b1539a9a783cf26e2f54feda92ec6d725da9 Mon Sep 17 00:00:00 2001 From: "Jose F. Morales" Date: Mon, 7 Mar 2022 03:44:45 +0100 Subject: [PATCH] (builder) using prebuilt docs in curl-based installation skips doc gen Src-commit: c977c1e318c3925ac65e400b54691bf281ce979a --- ciao-boot.sh | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/ciao-boot.sh b/ciao-boot.sh index 5afbb47a1..5912c22a1 100755 --- a/ciao-boot.sh +++ b/ciao-boot.sh @@ -48,17 +48,15 @@ release_query_info() { if [ "$v__devenv" = "yes" ]; then a__prebuilt_bin=no # TODO: no prebuilt bin for devenv yet case "$tag" in - master) a__prebuilt_docs=no ;; - *) a__prebuilt_docs=yes ;; + master) a__prebuilt_docs=no; a__with_docs=yes ;; + *) a__prebuilt_docs=yes; a__with_docs=no ;; esac - a__with_docs=yes else case "$os$arch" in DARWINaarch64) a__prebuilt_bin=no ;; # TODO: not yet - *) a__prebuilt_bin=yes + *) a__prebuilt_bin=yes ;; esac - a__prebuilt_docs=no - a__with_docs=no + a__prebuilt_docs=no; a__with_docs=no fi }