aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib
diff options
context:
space:
mode:
authorThéo Zimmermann2019-07-23 19:45:10 +0200
committerThéo Zimmermann2019-07-23 19:45:10 +0200
commitd57f262bb39ebbcae630f1439377c51aaa41452b (patch)
tree0661b77ebcc2e70268358f92590282de6e136b10 /doc/stdlib
parent00abd9ed2ac31d0655fa1f07a919b9739c8ec5fb (diff)
parentb3c82cbe2b7feafb254af316b5c4a8032e8cf8b3 (diff)
Merge PR #10552: Fix a detail in 2 doc files for the under tactic
Reviewed-by: Zimmi48
Diffstat (limited to 'doc/stdlib')
0 files changed, 0 insertions, 0 deletions