aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/uGraph.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/uGraph.ml')
-rw-r--r--kernel/uGraph.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 9793dd881..00c0ea70d 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -910,3 +910,4 @@ let check_leq =
let check_leq_key = Profile.declare_profile "check_leq" in
Profile.profile3 check_leq_key check_leq
else check_leq
+