diff options
| author | Théo Zimmermann | 2019-02-13 18:33:46 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-14 10:25:01 +0100 |
| commit | 57c69e8b78df99e69a31c0a6129346915de5e38c (patch) | |
| tree | d200356b778cbf43f1dccb23e38a9418aba6164a /dev/ci/docker | |
| parent | aa2d7486702433c94bfd645d3a5f6575a9ee729f (diff) | |
Document the now_show tactic.
It was used in the standard library and the test-suite but undocumented so far.
Diffstat (limited to 'dev/ci/docker')
0 files changed, 0 insertions, 0 deletions