doc: increase border spacing in HTML tables

diff --git a/doc/texinfo.css b/doc/texinfo.css
index ce3d13090c0f577aacd94e4544d56c2a870e90d8..ea56b3b33cfaf70b3395e96133a807c9fb30c0e3 100644 (file)
--- a/doc/texinfo.css
+++ b/doc/texinfo.css
@@ -52,6 +52,7 @@ table {
   text-align: left;
   margin-left:auto;
   margin-right:auto;
+  border-spacing: 7px;
   width: 50%;
 }