diff options
| author | Jim Fehrle | 2019-05-12 17:44:04 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-05-13 11:07:48 -0700 |
| commit | 5e1238260c32227f8568fb1328f922cdeaa8dfc8 (patch) | |
| tree | 6d21045fc8826d75580d4f06dc79ef6d76bac094 /engine/ftactic.ml | |
| parent | 9f11eeefc204bdad029b66f30bc6c52377af63ae (diff) | |
Handle tags shorter than "diff." without an exception
Diffstat (limited to 'engine/ftactic.ml')
0 files changed, 0 insertions, 0 deletions