diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-23 15:28:36 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-23 15:29:29 +0200 |
| commit | b28bafb1d2003558c916c75d36784f94e9aa1684 (patch) | |
| tree | 73d616a542aa2d22c760cadb515fb43675115043 /kernel/cbytecodes.mli | |
| parent | 85fbcf9ed5c2f080e83f52fd2cd1791fb4172e74 (diff) | |
Fix `Pp` function used by the `Info` command.
I used a low-level function, now changed to `msg_notice`.
Diffstat (limited to 'kernel/cbytecodes.mli')
0 files changed, 0 insertions, 0 deletions