diff options
| author | Emilio Jesus Gallego Arias | 2019-06-09 14:15:25 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-09 14:15:25 +0200 |
| commit | db0e1323d54caa3331368f6e17633475a8bb871c (patch) | |
| tree | 54665c1648eab90a5f8f9f3caa9fc9465f6f1d08 /doc/plugin_tutorial/tuto0 | |
| parent | a999ff029d7eca67531adfb4c7d6aeb0390e50b9 (diff) | |
| parent | 6f05a46e08fdb8de2319c36f07a737b1acebfe31 (diff) | |
Merge PR #10245: Command line: adding variants for Require, aligning on the vernac syntax
Reviewed-by: cpitclaudel
Reviewed-by: ejgallego
Ack-by: herbelin
Diffstat (limited to 'doc/plugin_tutorial/tuto0')
0 files changed, 0 insertions, 0 deletions