summaryrefslogtreecommitdiff
path: root/src/util.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/util.ml')
-rw-r--r--src/util.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/util.ml b/src/util.ml
index 5502398..5155fd7 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -1,5 +1,7 @@
open Unix
+let (@@) a b = a b
+
type id = int * int
let new_id () : id = (Random.int 100000, Random.int 100000)
let id_str (a, b) = Format.sprintf "%d.%d" a b