diff options
| author | mdenes | 2013-10-28 20:32:41 +0000 |
|---|---|---|
| committer | mdenes | 2013-10-28 20:32:41 +0000 |
| commit | 1e301c9921a8b24e52e05fdcc7a92f67f99ba31c (patch) | |
| tree | 7fda8c7fd32e28f2d98c83d3ff505095afdfabac /dev | |
| 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 'dev')
0 files changed, 0 insertions, 0 deletions