update manual to current state of code
authorChristian Grothoff <christian@grothoff.org>
Fri, 21 Jun 2019 20:40:40 +0000 (22:40 +0200)
committerChristian Grothoff <christian@grothoff.org>
Fri, 21 Jun 2019 20:40:40 +0000 (22:40 +0200)
commitd9e1a8e92cfd95e8f5dba3e5bc000de9b9cf49ac
tree471d97281594a5c45057d995f37ba8c2155f6bf9
parent56436c888427d7963e9ce3304cc33bc17fb89573
update manual to current state of code
doc/handbook/chapters/user.texi