diff options
| author | Théo Zimmermann | 2020-04-27 18:00:57 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-27 18:00:57 +0200 |
| commit | c47bc405275010e442402ead0f843014b7dab3c3 (patch) | |
| tree | e37ebed5d45ef25b92f26cd57754941c8fd07f7e /ide/protocol/xml_parser.ml | |
| parent | e0d7b05789d7c6d341d3001c227d99a278743fd1 (diff) | |
Fix an ordering bug in the CODEOWNERS file following #11529.
Diffstat (limited to 'ide/protocol/xml_parser.ml')
0 files changed, 0 insertions, 0 deletions