Index: 07_devmap.html
===================================================================
--- 07_devmap.html	(revision 289)
+++ 07_devmap.html	(revision 290)
@@ -150,10 +150,8 @@
 A common device map file will usually have a pinmap attribute that will
 set at least one attributes on each terminal.
 
-
-<p>{des7:22}
 <p><table border=1 cellspacing=0>
-<tr><th colspan=3 bgcolor="#aaaaaa"> {des7:23} device mapping related symbol attributes
+<tr><th colspan=3 bgcolor="#aaaaaa"> {des7:22} device mapping related symbol attributes
 <tr><th> attribute <th> value  <th> description
 <tr><td> devmap    <td> name   <td> name of the devmap file to use
 </table>