diff options
| author | Enrico Tassi | 2016-08-17 09:33:03 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-08-17 09:33:03 +0200 |
| commit | 8e79ac5a766e42dfbfc629087455c9bd7639402c (patch) | |
| tree | 95e7c9438c82574570fec1b1074a2a2a6a37e7ff /kernel/nativelambda.ml | |
| parent | 6c65822cd241ea2f5c552f8b685490aed86eecb1 (diff) | |
infoH: output via msg_* to make the XML protocol happy
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions