diff options
Diffstat (limited to 'otherlibs/dynlink/dynlink.ml')
| -rw-r--r-- | otherlibs/dynlink/dynlink.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/otherlibs/dynlink/dynlink.ml b/otherlibs/dynlink/dynlink.ml index 0d324a8540..d8d2f11623 100644 --- a/otherlibs/dynlink/dynlink.ml +++ b/otherlibs/dynlink/dynlink.ml @@ -18,6 +18,8 @@ open Dynlinkaux (* REMOVE_ME for ../../debugger/dynlink.ml *) open Cmo_format +let supported = true + type linking_error = Undefined_global of string | Unavailable_primitive of string @@ -33,6 +35,7 @@ type error = | File_not_found of string | Cannot_open_dll of string | Inconsistent_implementation of string + | Dynlink_not_supported exception Error of error @@ -268,6 +271,8 @@ let error_message = function "error loading shared library: " ^ reason | Inconsistent_implementation name -> "implementation mismatch on " ^ name + | Dynlink_not_supported -> + "dynlink not supported" let is_native = false let adapt_filename f = f |