diff options
| author | Hugo Herbelin | 2016-09-29 17:33:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-09-29 17:35:37 +0200 |
| commit | 14e47506ffabc43c25bf8da108abb6df78b803ad (patch) | |
| tree | d61c47fa21fddfa2c30727c0206c7576e21a9162 /kernel/nativecode.ml | |
| parent | 6d20e4c136fb2726ec8577bdfee051ecacdf8261 (diff) | |
Being more informative about the change of behavior of "subst".
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions