diff options
| author | Hugo Herbelin | 2016-04-17 11:50:33 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 21:55:47 +0200 |
| commit | 0d56fda01ecf8b38ef5f9a1fd3552f025972fbcd (patch) | |
| tree | 5c8266aa94cc1097b18535eda4ef9eb40ea21249 /plugins/rtauto | |
| parent | e9abd74adc486c1c1793754fdf83a33fe7b1b34c (diff) | |
Protect printing of ltac's "context [...]" from possible collision
with user-level notations by inserting spaces.
Diffstat (limited to 'plugins/rtauto')
0 files changed, 0 insertions, 0 deletions