Ticket #14606: 14606_gap_race.patch

File 14606_gap_race.patch, 1.2 KB (added by jdemeyer, 9 years ago)

  • sage/interfaces/gap.py 

    # HG changeset patch
# User Jeroen Demeyer <jdemeyer@cage.ugent.be>
# Date 1368864647 -7200
# Node ID b9c56af6ae6889b207c8e90656b8df2874ba7dda
# Parent  1dc9f8e6974aac70f42cdb909141b7afddac7faf
Catch OSErrors when removing GAP workspaces

diff --git a/sage/interfaces/gap.py b/sage/interfaces/gap.py
    a b  
    14801480    now = time.time()
    14811481    for F in os.listdir(GAP_DIR):
    14821482        if F.startswith('workspace-'):
    1483             age = now - os.path.getatime(os.path.join(GAP_DIR, F))
    1484             if age >= 604800:    # 1 week in seconds
    1485                 os.unlink(os.path.join(GAP_DIR, F))
     1483            W = os.path.join(GAP_DIR, F)
     1484            try:
     1485                age = now - os.path.getatime(W)
     1486                if age >= 604800:    # 1 week in seconds
     1487                    os.unlink(W)
     1488            except OSError:
     1489                # It's not a problem if W doesn't exist, everything
     1490                # else is an error.
     1491                if os.path.exists(W):
     1492                    raise
    14861493       
    14871494    # Create new workspace with filename WORKSPACE
    14881495    g = Gap(use_workspace_cache=False, max_workspace_size=None)