Ticket #13681: 13681_scripts.patch

File 13681_scripts.patch, 1.3 KB (added by jdemeyer, 9 years ago)
  • sage-cleaner

    # HG changeset patch
    # User Jeroen Demeyer <jdemeyer@cage.ugent.be>
    # Date 1351964647 -3600
    # Node ID 839f01c5a3635b7dbba19d87bae9f053b92b6f10
    # Parent  a8a59813314c013aa62496c2b325a1ea57f58487
    Correct temporary directory in sage-cleaner
    
    diff --git a/sage-cleaner b/sage-cleaner
    a b  
    33#########################################################
    44# This is the sage monitor *daemon*, which cleans up after SAGE.
    55# Some things that it cleans up:
    6 #   * $HOME/.sage/temp/pid directories
     6#   * $HOME/.sage/tmp/pid directories
    77#   * Processes that SAGE spawns.  If a copy of SAGE isn't
    88#     running, then any process it spawned should have its
    99#     process group killed
     
    2323HOSTNAME = socket.gethostname().replace('-','_').replace('/','_').replace('\\','_')
    2424
    2525DOT_SAGE = os.environ['DOT_SAGE']
    26 tmp = '%s/temp/%s/'%(DOT_SAGE, HOSTNAME)
     26tmp = os.path.join(DOT_SAGE, 'tmp', HOSTNAME)
    2727try:
    2828    os.makedirs(tmp)
    2929except OSError:
     
    8787            # try again later
    8888            killed_them_all = False
    8989    return killed_them_all
    90            
    91                
    9290
    9391
    94 pidfile = '%s/temp/cleaner-%s.pid'%(DOT_SAGE, HOSTNAME)
     92pidfile = os.path.join(DOT_SAGE, 'tmp', 'cleaner-%s.pid'%HOSTNAME)
    9593def setup_daemon():
    9694    if os.path.exists(pidfile):
    9795        pid = open(pidfile).read()