From 8359701a67e2e2fd1026ef958d1395807a93489c Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 2 Mar 2020 19:37:21 +0000
Subject: Fix jenkins

---
 src/value.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/value.ml b/src/value.ml
index 11cda94b..7dfa380d 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -701,7 +701,7 @@ let primops = ref
        ("ones", value_ones);
        ("shiftr", value_shiftr);
        ("shiftl", value_shiftl);
-       ("arith_shiftr", value_shiftr);
+       ("arith_shiftr", value_arith_shiftr);
        ("shift_bits_left", value_shift_bits_left);
        ("shift_bits_right", value_shift_bits_right);
        ("add_int", value_add_int);
-- 
cgit v1.2.3