diff options
| author | Hugo Herbelin | 2017-02-23 14:58:17 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-02-23 14:58:48 +0100 |
| commit | 8451b4ae99b448894a6269c08be7f3ac0d74cac4 (patch) | |
| tree | 2846fada2c230bc996d3afe5aaeb0db51c00e953 /kernel/nativecode.ml | |
| parent | fedc831df9626a31cd0d26ee6b9e022b67f90c2a (diff) | |
Fixing a little bug in printing ex2 (type was printed "_" by default).
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions