aboutsummaryrefslogtreecommitdiffhomepage
path: root/caching-tests/bench.urs
diff options
context:
space:
mode:
authorGravatar Ziv Scully <ziv@mit.edu>2015-11-17 04:08:12 -0500
committerGravatar Ziv Scully <ziv@mit.edu>2015-11-17 04:08:12 -0500
commitde5089fc5dfb8904ad3a8e36f042ce234ac9340b (patch)
treecee1595f198ba7db55df574115f548815cf60c02 /caching-tests/bench.urs
parent39804bcf37a35ca6a2cb5e49849ce9453c9025bc (diff)
Ran a benchmark!
Diffstat (limited to 'caching-tests/bench.urs')
-rw-r--r--caching-tests/bench.urs3
1 files changed, 2 insertions, 1 deletions
diff --git a/caching-tests/bench.urs b/caching-tests/bench.urs
index 0f780541..5f3d2ee8 100644
--- a/caching-tests/bench.urs
+++ b/caching-tests/bench.urs
@@ -1 +1,2 @@
-val main : int -> int -> transaction page
+val check : int -> transaction page
+val flush : int -> transaction page