Ticket #9811: trac_9811-use_pipestatus_in_sage-sage.scripts.patch

File trac_9811-use_pipestatus_in_sage-sage.scripts.patch, 1.7 KB (added by leif, 8 years ago)

SCRIPTS repo. Based on Sage 4.7.2.alpha4.

  • sage-sage

    # HG changeset patch
    # User Leif Leonhardy <not.really@online.de>
    # Date 1318514918 -7200
    # Node ID 58c82036cc304ebc4b3fec4c3943faded4299a44
    # Parent  91cf96ce5ec439b2c489c72e479fb63d67d4cbb7
    #9811: Use 'pipestatus' in 'sage-sage' when installing packages; other small improvements.
    
    Using 'pipestatus' is necessary to get the exit code of 'sage-spkg'
    (rather than 'tee').  (Previously 'sage -i nonexistent' returned 0.)
    
    diff --git a/sage-sage b/sage-sage
    a b  
    791791   fi
    792792   for PKG in "$@"
    793793   do
    794        echo "Calling sage-spkg on $PKG"
    795        PKG_NAME=`echo "$PKG" | sed -e "s/\.spkg$//"`
    796        PKG_NAME=`basename "$PKG_NAME"`
    797        case $PKG in
    798            /*)
    799                sage-spkg $OPT "$PKG" 2>&1 | (trap "" SIGINT; tee -a ../install.log "$SAGE_LOGS/$PKG_NAME".log)
    800            ;;
    801            *)
    802                sage-spkg $OPT "$CUR/$PKG" 2>&1 | (trap "" SIGINT; tee -a ../install.log "$SAGE_LOGS/$PKG_NAME".log)
    803            ;;
    804        esac
    805 
    806        if [ $? -ne 0 ]; then
    807           exit 1
    808        fi
    809        shift
     794        echo "Calling sage-spkg on '$PKG'"
     795        PKG_NAME=`echo "$PKG" | sed -e "s/\.spkg$//"`
     796        PKG_NAME=`basename "$PKG_NAME"`
     797        case "$PKG" in
     798            /*) PKG_PATH="$PKG";;
     799            *) PKG_PATH="$CUR/$PKG";;
     800        esac
     801        # Could use ./pipestatus here, but using an absolute path is safer:
     802        # (We'll have to change it anyway in case 'pipestatus' one day moves.)
     803        "$SAGE_ROOT"/spkg/pipestatus \
     804            "sage-spkg $OPT '$PKG_PATH' 2>&1" \
     805            "(trap '' SIGINT; tee -a '$SAGE_ROOT'/install.log '$SAGE_LOGS/$PKG_NAME'.log)"
     806        # Do not try to install further packages (if any) if one failed:
     807        if [[ $? -ne 0 ]]; then
     808            echo >&2 "Error: Failed to install package '$PKG_NAME'."
     809            exit 1
     810        fi
     811        shift
    810812   done
    811813   exit $?
    812814}