diff options
| author | Emilio Jesus Gallego Arias | 2019-04-10 02:18:15 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-10 03:37:48 +0200 |
| commit | 78259a079da05b691d0cad87c70a446568427697 (patch) | |
| tree | 78f8e14730b55cc4cd9a7f91d627ad9d9f67fd94 /doc/plugin_tutorial | |
| parent | e3e3e6949f1c80abec9942ee0d258b58e5a7d382 (diff) | |
[coqdep] Exit with error code on exception.
This turns out to confuse many tools otherwise.
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions