update index page
authorChristian Grothoff <christian@grothoff.org>
Sun, 7 Jul 2019 18:30:38 +0000 (20:30 +0200)
committerChristian Grothoff <christian@grothoff.org>
Sun, 7 Jul 2019 18:30:38 +0000 (20:30 +0200)
commit71a107e3dfbbd7d42a74ab63bfbfb451c43bbd19
tree8976bb011d3a954e823571e760495af63a087548
parentbc67657528b7e52c9c5e5a7603008ac22815e741
update index page
doc/handbook/index.html