diff options
| author | Pierre-Marie Pédrot | 2021-04-19 12:05:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-04-19 12:05:38 +0200 |
| commit | 9d3ea20fb8e9f1c3acfa3d127a1e3ee99fe7ebc9 (patch) | |
| tree | bf7a761119e9309d2da0840a1edc0e10882e515e /dev | |
| parent | 9fe4108289f584461b5dc7af08095d6279a222af (diff) | |
Slightly tweak the not-unit Ltac2 warning.
Fixes #11683.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions