diff options
| author | Pierre-Marie Pédrot | 2016-03-15 19:47:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-15 19:48:53 +0100 |
| commit | e5b40d615d0ed9819f6ac8345ed924d8a501172e (patch) | |
| tree | d6d498ac9edeb97fe96fd6f06015b10ee5c871a1 /lib/system.ml | |
| parent | 45e43916a7ce756b617b7ba3f8062f7956872fb3 (diff) | |
CoqIDE is more resilient to initialization errors.
We force the STM to finish after the initialization request so as to raise
exceptions that may have been generated by the initialization process. Likewise,
we simply die when the initialization request fails in CoqIDE instead of just
printing an error message.
This is the fix for the underlying issue of bug #4591, but it does not solve
the bug yet.
Diffstat (limited to 'lib/system.ml')
0 files changed, 0 insertions, 0 deletions