diff options
| author | Jason Gross | 2017-12-11 02:36:50 -0500 |
|---|---|---|
| committer | Jason Gross | 2017-12-11 18:18:27 -0500 |
| commit | f912708d039a0ea5d1af71b15585abcc5ac0e800 (patch) | |
| tree | 7d7ed2509951f344902b6be8605a4773a7092dde /API/API.ml | |
| parent | 54a9d18913db05c29837f60b4d82935207ec483a (diff) | |
Use msg_info for LtacProf
This way, `Time Show Ltac Profile` shows the profile in `*response*` in
PG, without an extra `infomsg` tag on the timing.
Diffstat (limited to 'API/API.ml')
0 files changed, 0 insertions, 0 deletions