diff options
| author | Hugo Herbelin | 2016-04-09 16:39:55 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-09 18:26:00 +0200 |
| commit | a2664de27eabbba7fc357305679112aef99e1f74 (patch) | |
| tree | ad434de76d480c744d1ed8f22308c7abef143590 /kernel | |
| parent | 41af4c3e36af15d9cc235cb5effedeed40478d2e (diff) | |
Removing automatic printing of leading space in auto_using and
hintbases so that it does not put extra space when auto is defined as
a TACTIC EXTEND.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions