diff options
| author | Emilio Jesus Gallego Arias | 2020-03-07 14:24:07 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-19 17:18:55 -0400 |
| commit | fb1625d723a4eb44c9a5266c759916b735e69b74 (patch) | |
| tree | 4bc9f4fabb777adafd88da2ac7b6c7d149ddb1b5 /plugins/syntax/float_syntax.ml | |
| parent | e2e4912212c5f6ab94eaded61e53b0478f9b17c8 (diff) | |
[obligations] Refactor some common code on save path
Both the interactive and non-interactive save path share some internal
table update code.
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions