diff options
| author | Gaëtan Gilbert | 2019-10-28 17:55:23 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-31 14:42:54 +0100 |
| commit | 82bdd64c97f45510044a9ccd9b5b87effcd034d1 (patch) | |
| tree | 9c95727492317912b89966d93ef1aaca45cf7e5e /kernel/nativelambda.mli | |
| parent | 215b7e43cba768bfc82914718b159a22797f9d2b (diff) | |
Print argument info as an Arguments command in About
Close #10961
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions