Ticket #12486: patchbot-root-5.0.patch

File patchbot-root-5.0.patch, 564 bytes (added by ddrake, 9 years ago)

for 5.0 series, apply to SAGE_ROOT repo

  • spkg/bin/sage 

    # HG changeset patch
# User Robert Bradshaw <robertwb@math.washington.edu>
# Date 1328866496 28800
# Node ID bc2b7ff3d7f2896dd24acb2898b168855297420a
# Parent  ba6824cfc2b245e08cd82477f7a153b21c499075
trac #12486: add patchbot to Sage. Apply to SAGE_ROOT repo.

diff --git a/spkg/bin/sage b/spkg/bin/sage
    a b  
    755755   exit $?
    756756fi
    757757
     758if [ "$1" = '-patchbot' -o "$1" = "--patchbot" ]; then
     759   shift
     760   $SAGE_LOCAL/bin/patchbot/patchbot.py "$@"
     761   exit $?
     762fi
     763
    758764if [ "$1" = '-c' ]; then
    759765   cd "$CUR"
    760766   shift