diff options
| author | Hugo Herbelin | 2017-04-03 15:59:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-04-07 09:22:23 +0200 |
| commit | bd76257f84dcaef90498a85342077a743855f565 (patch) | |
| tree | 33ebcf841f5b78a99c7e9f1578da3fd37edc42cc /kernel/nativecode.ml | |
| parent | b1cd93c7ad0f550077a62a1c7cb6915041c6c85e (diff) | |
Turning the printing primitive projection parameter flag off by default.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions