aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-10-18 15:24:30 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-10-18 16:02:36 +0200
commitf8c0dbb29d260f9be0f188358d8d53145976a177 (patch)
treee5c4a5fadee879cac1993e8261b9d604edde3673 /library
parent0ac62afd4b2a8ce220c70b71f6a8d34445de6528 (diff)
Fixing link to GitHub issue search, and wording.
Diffstat (limited to 'library')
0 files changed, 0 insertions, 0 deletions