diff options
| author | Pierre Courtieu | 2014-12-15 20:56:07 +0100 |
|---|---|---|
| committer | Pierre Courtieu | 2014-12-15 20:56:15 +0100 |
| commit | 0e730e4fa316cbfbd2d6dc60276498f57f500e0e (patch) | |
| tree | a3149569f71bdc4ee842ec49b8d6d98c126c7102 /kernel/nativelib.mli | |
| parent | 594d2b8beb98b67f059014c5d76ba0d09dba2e4c (diff) | |
Changed bullet informations to warning for better display in PG.
Since it displays together with the goal, it is better (for pg and
other interfaces probably) that they are in a different message.
Diffstat (limited to 'kernel/nativelib.mli')
0 files changed, 0 insertions, 0 deletions