fix
authorChristian Grothoff <christian@grothoff.org>
Fri, 21 Jun 2019 22:46:44 +0000 (00:46 +0200)
committerChristian Grothoff <christian@grothoff.org>
Fri, 21 Jun 2019 22:46:44 +0000 (00:46 +0200)
commitbf58fd078b2f6b5199df65ba694b16840bc602ac
tree6ef57a0500fc511d068609283b39a6fb4c8efa49
parentf37f5b281184efba9929ff0453079f1795573671
fix
doc/handbook/chapters/user.texi