diff options
| author | Pierre-Marie Pédrot | 2020-08-27 16:23:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-27 16:23:44 +0200 |
| commit | 2062f9cd5ce3c17c128186d1e9e2193528941e5c (patch) | |
| tree | edd7cf41caeedae18d60dc5c859e2532884ab80a /plugins/syntax/float_syntax.ml | |
| parent | 829d7ac10175c41eaf3ce8ad9531abeab713dcba (diff) | |
| parent | bd00733ef04e4c916ab4a00d80e9ee1142bcd410 (diff) | |
Merge PR #12499: Clean future goals
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: mattam82
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions