diff options
| author | Théo Zimmermann | 2016-10-19 14:18:52 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2016-10-19 14:18:52 +0200 |
| commit | 5be957316c23db6366aefc246d1d24480aa2f1ea (patch) | |
| tree | c755c1b3208b229bde7d530cc6a933c3b1a5e5fa /dev | |
| parent | 8d77523f8883fae56a8a338060bb2a52b0fd566c (diff) | |
Making the doc of auto hints more precise.
The doc of auto hints now mention again that sometimes a hint
will be used with simple apply and sometimes it will be used
with exact.
It does not try to be fully precise in that we don't
necessarily want to document the behaviors of auto that
we might like to change.
See also the discussion on commit 9227d6e.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions