diff options
Diffstat (limited to 'utils/misc.ml')
| -rw-r--r-- | utils/misc.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/utils/misc.ml b/utils/misc.ml index 0eab66dc5..c75ac3130 100644 --- a/utils/misc.ml +++ b/utils/misc.ml @@ -195,3 +195,7 @@ let rev_split_words s = | _ -> split2 res i (j+1) end in split1 [] 0 + +let get_ref r = + let v = !r in + r := []; v |