diff options
| author | Hendrik Tews | 2020-11-20 23:38:22 +0100 |
|---|---|---|
| committer | Hendrik Tews | 2020-12-07 14:56:32 +0100 |
| commit | abfcd41041f5ba00d9d8f007808d67a312fbe8c4 (patch) | |
| tree | 376693a89bc9dad20f31712ef0d1b1f3293efaf0 /pgshell | |
| parent | 1689a494635fce5fbbadbdc3bed50299fd7521ab (diff) | |
protect coq-callcoq against escaping signals
This hopefully fixes compilation without coqtop and especially
the github tests.
Diffstat (limited to 'pgshell')
0 files changed, 0 insertions, 0 deletions