minor fix
authorSchanzenbach, Martin <mschanzenbach@posteo.de>
Tue, 15 Oct 2019 08:40:00 +0000 (10:40 +0200)
committerSchanzenbach, Martin <mschanzenbach@posteo.de>
Tue, 15 Oct 2019 08:40:00 +0000 (10:40 +0200)
commit36f25e7ccdee5c319a6bd77949f01453c8a5a69e
treebadc0d5d24a61d85bfc466d6c433c56b56c37081
parent096579cbd720bb0b6d0f974cdf0765cf0fdcfca4
minor fix
doc/handbook/chapters/user.texi