Admin/components/index.php
changeset 72542 c588e0b8b8b0
parent 72503 05d0977ec706
--- a/Admin/components/index.php	Mon Nov 02 13:59:05 2020 +0100
+++ b/Admin/components/index.php	Mon Nov 02 16:50:22 2020 +0100
@@ -1,11 +1,11 @@
 <html>
 <body>
-<h2>Components:</h2>
+<h2>Isabelle Components</h2>
 <table>
 <tr>
-<th> Name </th>
-<th> &nbsp;&nbsp;&nbsp; </th>
-<th> Size</th>
+<td><b>Name</b></td>
+<td>&nbsp;&nbsp;&nbsp;</td>
+<td><b>Size</b></td>
 </tr>
 <?php
  $component_pattern="/^.+\.tar\.gz$/";
@@ -14,7 +14,7 @@
    if (preg_match($component_pattern, $file)
        && is_file($file)
        && is_readable($file)) {
-     print "<tr><td><a href=\"$file\">$file</a></td><td></td><td>".filesize($file)."</td></tr>\n";
+     print "<tr><td><a href=\"$file\"><code>$file</code></a></td><td></td><td>".filesize($file)."</td></tr>\n";
   }
  }
 ?>