diff options
| author | Pierre-Marie Pédrot | 2015-04-10 15:13:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-04-10 15:13:37 +0200 |
| commit | ba6f6500a948985b091cbf6a05d3631490465081 (patch) | |
| tree | 6cba268852bbedfc3802417d8e57a770b313d012 /plugins | |
| parent | 33650e275a4b3f00541ea87ee4b39892be5fdb2f (diff) | |
Making the hints for the auto tactics private.
They are all generated by the Hints module, and making them purely opaque is
not worthwhile because we project them a lot. This ensures that they all get
generated following a uniform process.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions