diff options
| author | Guillaume Melquiond | 2019-07-23 11:12:05 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2019-07-29 21:30:59 +0200 |
| commit | 7ebc836e8a526918ac647acff60f83517276f4da (patch) | |
| tree | e8c8e8275a9699c533a21297f27604e53ccf2fef /doc/plugin_tutorial/tuto2/src/persistent_counter.ml | |
| parent | 807b1e18575914f9956569ab71bb5fe29716cbdf (diff) | |
Use a more traditional definition for uint63_div21 (fixes #10551).
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src/persistent_counter.ml')
0 files changed, 0 insertions, 0 deletions