equal
deleted
inserted
replaced
10 |
10 |
11 class LockHeld(Exception): |
11 class LockHeld(Exception): |
12 pass |
12 pass |
13 |
13 |
14 class lock: |
14 class lock: |
15 def __init__(self, file, wait=1): |
15 def __init__(self, file, wait=1, releasefn=None): |
16 self.f = file |
16 self.f = file |
17 self.held = 0 |
17 self.held = 0 |
18 self.wait = wait |
18 self.wait = wait |
|
19 self.releasefn = releasefn |
19 self.lock() |
20 self.lock() |
20 |
21 |
21 def __del__(self): |
22 def __del__(self): |
22 self.release() |
23 self.release() |
23 |
24 |
41 raise LockHeld(util.readlock(self.f)) |
42 raise LockHeld(util.readlock(self.f)) |
42 |
43 |
43 def release(self): |
44 def release(self): |
44 if self.held: |
45 if self.held: |
45 self.held = 0 |
46 self.held = 0 |
|
47 if self.releasefn: |
|
48 self.releasefn() |
46 try: |
49 try: |
47 os.unlink(self.f) |
50 os.unlink(self.f) |
48 except: pass |
51 except: pass |
49 |
52 |