diff options
| author | Daniel R. Grayson | 2015-01-27 08:50:07 -0600 |
|---|---|---|
| committer | Hugo Herbelin | 2015-03-18 18:13:22 +0100 |
| commit | 8eeef779da833c28e4955f71ec95077138dcb71f (patch) | |
| tree | d62a501f3733f7be2e14e5cb072f4fe45c0e8158 /kernel/modops.ml | |
| parent | 623a0e9bc07f19dacd8a25c33ebf1e68d9b3be30 (diff) | |
add -type-in-type to the usage message
Diffstat (limited to 'kernel/modops.ml')
0 files changed, 0 insertions, 0 deletions