aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorThéo Zimmermann2020-04-03 10:27:15 +0200
committerGitHub2020-04-03 10:27:15 +0200
commit8ac8f5aa327ca8de66e90bb33d1950d9a4749177 (patch)
tree1fa9917ed1d1a8ea74b8cf000155426190523b89 /lib
parente3e1133fe5685213460a6cc3f761283815223e3d (diff)
Update doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions