diff options
| author | coqbot-app[bot] | 2021-01-27 08:34:33 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-27 08:34:33 +0000 |
| commit | 0c185094d40d10dc43f1432ef708a329fae25751 (patch) | |
| tree | f322ca666b1beb02e7a9d4d8195dc434f6593e4c /sysinit/usage.ml | |
| parent | 7308d118879dcc603c45008c3d106ba3688f4e2b (diff) | |
| parent | 028342741eee445c44db2661b1c246623c96e01a (diff) | |
Merge PR #13785: [coqargs] use the standard option injection system for -w
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Diffstat (limited to 'sysinit/usage.ml')
0 files changed, 0 insertions, 0 deletions