diff options
| author |  mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-28 20:32:41 +0000 |
|---|---|---|
| committer | mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-28 20:32:41 +0000 |
| commit | 1e301c9921a8b24e52e05fdcc7a92f67f99ba31c (patch) | |
| tree | 7fda8c7fd32e28f2d98c83d3ff505095afdfabac /kernel/nativelib.ml | |
| parent | 3c36e46caf34e5033ba9378674caee0efa93d809 (diff) | |
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
Diffstat (limited to 'kernel/nativelib.ml')
| -rw-r--r-- | kernel/nativelib.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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. *) |