diff options
| author | Clément Pit-Claudel | 2020-02-29 13:04:59 -0500 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-02-29 13:04:59 -0500 |
| commit | ed8ac4195c89ee14d03c80e1d9d3f66665573cbf (patch) | |
| tree | aae1024c25c7b5d7ed14348d78e2ef5c45ebb1d6 /plugins/syntax/float_syntax.ml | |
| parent | 7c1d1a58697486f4f52ac7f45b932d03a7e77e5c (diff) | |
| parent | fb9b5c392672eebf97451802ee292505b4c46fec (diff) | |
Merge PR #11701: Fix #11696: link from refman to stdlib doc is dead.
Reviewed-by: cpitclaudel
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions