diff options
| author | Vincent Laporte | 2019-07-29 13:48:06 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-07-29 14:21:32 +0000 |
| commit | 2802a98273bd1478113130a235bf406d2f7f73f5 (patch) | |
| tree | 2419cffdb0c796fb1f49b2a7ed8ebda84a95ed03 /dev | |
| parent | b409b9793ba6219053818ac203c95e6bf87f0608 (diff) | |
Document changes by PR 10324
White spaces are forbidden in the “&ident” syntax for ltac2 references.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions