diff options
| author | Jim Fehrle | 2021-04-17 13:07:41 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2021-04-17 13:07:41 +0200 |
| commit | c20769ad4851ee7fa99605fed6b89964e147cddc (patch) | |
| tree | a588c52a02655dce4422155d47cbb7523754f402 /kernel/nativelibrary.ml | |
| parent | b55216ab3509f48e45aac035f1b799529d068f51 (diff) | |
Remove superfluous sort.
Removing it makes no difference to the order of glossary entries,
which is determined by the "for ... sorted" statement above.
Diffstat (limited to 'kernel/nativelibrary.ml')
0 files changed, 0 insertions, 0 deletions