diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-05 18:27:24 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-05 18:27:24 +0200 |
| commit | 6c177d95f4e7d3179db1732f1ba1bda43a83393f (patch) | |
| tree | a201827ca42ae9148585c575ede2c0f2dc30dc89 /ide/xml_printer.ml | |
| parent | 8ce4b0d7d16fe134d8621efc9d557ba3e9686b0f (diff) | |
| parent | 05bd0ab1dd85764874ca077005dcaff5414589a5 (diff) | |
Merge PR #1102: On the detection of evars which "advanced" (and a fix to BZ#5757)
Diffstat (limited to 'ide/xml_printer.ml')
0 files changed, 0 insertions, 0 deletions