12 lines
312 B
Diff
12 lines
312 B
Diff
--- ./src/numeric_plugins/mlgmp_plugin.ml.orig 2013-02-14 04:08:25.000000000 -0700
|
|
+++ ./src/numeric_plugins/mlgmp_plugin.ml 2013-02-19 13:56:39.613438907 -0700
|
|
@@ -19,7 +19,7 @@
|
|
|
|
*)
|
|
|
|
-open Gmp
|
|
+open Mlgmp
|
|
|
|
let bits_of_string s =
|
|
let s' = String.sub s 2 ((String.length s)-2) in (* remove prefix "0b" *)
|