diff options
| author | Pierre-Marie Pédrot | 2019-04-11 10:12:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-04-11 10:12:49 +0200 |
| commit | 36c15766a9295d980d142da0e42aebf1309f4eb4 (patch) | |
| tree | aa60444139ed57aa969389eea9ccbf1ebedf4ea0 /kernel | |
| parent | ddf6dffe7d9afe635d32c41336345812f7c71139 (diff) | |
| parent | 78259a079da05b691d0cad87c70a446568427697 (diff) | |
Merge PR #9938: [coqdep] Exit with error code on exception.
Reviewed-by: ppedrot
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions