summaryrefslogtreecommitdiff
path: root/library/states.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/states.ml')
-rw-r--r--library/states.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/library/states.ml b/library/states.ml
index 3a4be1ca..b2ece049 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: states.ml 13175 2010-06-22 06:28:37Z herbelin $ *)
+(* $Id$ *)
open System
@@ -32,14 +32,14 @@ let (extern_state,intern_state) =
let with_heavy_rollback f x =
let st = freeze () in
- try
+ try
f x
with reraise ->
(unfreeze st; raise reraise)
let with_state_protection f x =
let st = freeze () in
- try
+ try
let a = f x in unfreeze st; a
with reraise ->
(unfreeze st; raise reraise)