diff options
| author | Gaëtan Gilbert | 2020-07-23 11:30:11 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-23 11:30:11 +0200 |
| commit | 667fac4add739479bc263f93f5c67f2c5414a865 (patch) | |
| tree | e01c0041e0b8dfb3ac3aa9ecbf9bc7a12b0f9878 /plugins/syntax/float_syntax.ml | |
| parent | 58df19e952f23ce9376c67f21d09e515a861db0c (diff) | |
| parent | b7d501fb22e6725da20c59b895e19d30b6b2ad50 (diff) | |
Merge PR #12672: Fix failing macOS build.
Ack-by: JasonGross
Reviewed-by: SkySkimmer
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions