diff options
| author | Pierre-Marie Pédrot | 2019-01-23 14:06:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-01-23 14:06:17 +0100 |
| commit | 2809b40d2b4c761df0c3ea2cd5bb35357eb99c97 (patch) | |
| tree | b3e002c1cbca0d624bd4dd5219d550616a4b9a64 /dev/include | |
| parent | bc943f0956496ed0e02de08a5a3a1b922423e72c (diff) | |
| parent | 945f49236e0db8179548110a056f9787ecffd746 (diff) | |
Merge PR #9347: At Qed, if shelved goals remain, emit a warning instead of an error
Ack-by: maximedenes
Reviewed-by: ppedrot
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions