diff options
| author | coqbot-app[bot] | 2020-10-08 20:47:34 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-08 20:47:34 +0000 |
| commit | 022632c074205bbe9fa3f992782e948c12cb7384 (patch) | |
| tree | 98c2efc4603615ef7035cb59115bb4fc29972a6d /dev/doc | |
| parent | e85f6b36711bf7214b2351724ea56b7808ab2321 (diff) | |
| parent | a2733be481563faff6505dd975a0a067ce28722a (diff) | |
Merge PR #12949: When a notation is only parsing, do not attach to it a specific format.
Reviewed-by: ejgallego
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions