diff options
| author | Théo Zimmermann | 2018-07-25 15:08:33 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-07-25 18:40:22 +0200 |
| commit | aee50066c9ef94ec2967e2f6f659ecb7a0f9598e (patch) | |
| tree | 36ce371524c40e6a7e9f850942065d75f3232089 /kernel/nativelambda.mli | |
| parent | 9b6ce4f1848c546d0d361aa1089fa2907ca4c9ad (diff) | |
[sphinx] Add a way of skipping names in the indexes.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions