diff options
| author | Emilio Jesus Gallego Arias | 2018-11-09 13:01:53 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-12 03:32:32 +0100 |
| commit | a8a3aeb49f3627a65c86c92b0ed743f7bfcf9ffb (patch) | |
| tree | 9f0e929522f2c46249200ff4e270833c014c0ec9 /clib/diff2.ml | |
| parent | 186d67228018a84a93de024971356249ddbde668 (diff) | |
[clib] Remove unneeded `get_extension` function.
This has been in OCaml since 4.04.
Diffstat (limited to 'clib/diff2.ml')
0 files changed, 0 insertions, 0 deletions