diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2015-02-19 11:28:19 +0100 |
---|---|---|
committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-02-24 16:37:04 +0100 |
commit | 50edb9bb8d43b190996d1d85a2bfd95f52b2db19 (patch) | |
tree | 52eb6f73a5c6f9c00ade4a4937960740972603ad /kernel/constr.mli | |
parent | ebf4d8e58eeddaf5237447a9a0f21de48e72caa5 (diff) |
[info_auto] & [info_trivial]: warning message to help users find [Info].
Diffstat (limited to 'kernel/constr.mli')
0 files changed, 0 insertions, 0 deletions