diff options
| author | coqbot | 2020-08-19 20:18:53 +0200 |
|---|---|---|
| committer | GitHub | 2020-08-19 20:18:53 +0200 |
| commit | b409b9837ce438042bb259d16a1b5156a2e0acb9 (patch) | |
| tree | c14c795848d67f59fcb0f390cd24acedbcb8af1e /plugins/syntax/float_syntax.ml | |
| parent | a18d81ce5e1f11b7b52651e5fbef0938ec871ac3 (diff) | |
| parent | 87d6d18a47fc8166029205bd9dadfc14dd22640c (diff) | |
Merge PR #12856: Adding a mention of the JSON extraction in the documentation.
Reviewed-by: jfehrle
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions