From 1e301c9921a8b24e52e05fdcc7a92f67f99ba31c Mon Sep 17 00:00:00 2001 From: mdenes Date: Mon, 28 Oct 2013 20:32:41 +0000 Subject: Native compiler: library compilation errors are now non fatal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16944 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/nativelib.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/nativelib.ml') diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index c9da5222f..49f84bc43 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -76,7 +76,7 @@ let compile ml_filename code = write_ml_code ml_filename code; call_compiler ml_filename (!get_load_paths()) -(* call_linker dynamic links code for constants in environment or a *) +(* call_linker links dynamically the code for constants in environment or a *) (* conversion test. Silently fails if the file does not exist in bytecode *) (* mode, since the standard library is not compiled to bytecode with default *) (* settings. *) -- cgit v1.2.3