diff options
| author | Hugo Herbelin | 2014-12-12 18:12:45 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-15 19:18:41 +0100 |
| commit | 9aa416c0c66ad7e14c4704898b74b99237d81c78 (patch) | |
| tree | 7b2519a4aa91a80c6c2c6e463389b13bbc5fa47e /plugins/syntax/string_syntax.ml | |
| parent | 4fec6bdf0ad0f49c98a82538c5caf4511ba5e95c (diff) | |
Documenting check_record + changing a possibly undefined int into int option.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions