aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/uint31.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/uint31.ml')
-rw-r--r--kernel/uint31.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/uint31.ml b/kernel/uint31.ml
index 0f1c1444b..fea12332c 100644
--- a/kernel/uint31.ml
+++ b/kernel/uint31.ml
@@ -149,5 +149,5 @@ let tail0 x =
if !x land 0x1 = 0 then ( r := !r + 1);
!r
-
-
+let add_digit x d =
+ (x lsl 1) lor d