diff options
| author | Hugo Herbelin | 2018-04-26 22:32:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-05-02 22:25:44 +0200 |
| commit | aae89bce1ca7c1a21b7eef345050dff5a9e88748 (patch) | |
| tree | 4fec1debf67d8625b4859bac8610b4c2d523119b /plugins/syntax/string_syntax.ml | |
| parent | fd146ca38202c9843b4240cbdac0ae75f57e4d67 (diff) | |
Reporting when an error occurs at initialization time.
Done by simplifying the three "try" liable to be caught at
initialization time into one and by ensuring that the remaining one
reports about being in initialization phase.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions