diff options
| author | whitequark | 2018-06-21 03:29:14 +0000 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-16 17:43:14 +0100 |
| commit | 54930207d4e0ba22ef079b36e89cd2c1287760f7 (patch) | |
| tree | 8a6c5b79916dfb0b5bf1a98dd018fbd02aa810d6 /Makefile.dev | |
| parent | 778213b89d893b55e572fc1813c7209d647ed6b0 (diff) | |
Add Dyn.anonymous, a more efficient version of Dyn.create (string_of_int n).
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions