diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2014-12-15 20:56:07 +0100 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2014-12-15 20:56:15 +0100 |
| commit | 0e730e4fa316cbfbd2d6dc60276498f57f500e0e (patch) | |
| tree | a3149569f71bdc4ee842ec49b8d6d98c126c7102 /kernel/nativeconv.ml | |
| 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/nativeconv.ml')
0 files changed, 0 insertions, 0 deletions