diff options
| author | Hugo Herbelin | 2014-07-01 10:53:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-07-01 11:55:03 +0200 |
| commit | f8e74d5baa18513fb8f697aaa7e8a495c9a2a9d5 (patch) | |
| tree | 9024ff3277016995cf3e03a6ffd8f3b3316e677f /kernel | |
| parent | d755f77f9cc4760c403e588aea085733cd1f2979 (diff) | |
Fixing the place where to insert a space in "Tactic failure"
message. Otherwise, a heading space was missing when calling tclFAIL
from ML tactics.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions