diff options
Diffstat (limited to 'plugins/extraction/common.ml')
| -rw-r--r-- | plugins/extraction/common.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 099a22408a..4ab1ac2fba 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -692,7 +692,7 @@ let is_native_string c = (* Extract the underlying string. *) -let rec get_native_string c = +let get_native_string c = let buf = Buffer.create 64 in let rec get = function (* "EmptyString" constructor *) |