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/nativelib.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/nativelib.ml')
0 files changed, 0 insertions, 0 deletions