minor extensions
authorhaftmann
Wed, 05 Apr 2006 17:38:32 +0200
changeset 19338 952b12ebfdff
parent 19337 146b25b893bb
child 19339 59f08f67ed3f
minor extensions
Admin/website/build/pypager.py
Admin/website/css/isabelle_screen.css
--- a/Admin/website/build/pypager.py	Wed Apr 05 12:47:38 2006 +0200
+++ b/Admin/website/build/pypager.py	Wed Apr 05 17:38:32 2006 +0200
@@ -402,7 +402,7 @@
 
         loc, name = posixpath.split(systemId)
         if loc == u"http://www.w3.org/TR/xhtml1/DTD" or loc == u"":
-            systemId = path.join(self._dtd, name)
+            systemId = path.abspath(path.join(self._dtd, name))
         return EntityResolver.resolveEntity(self, publicId, systemId)
 
     def processingInstruction(self, target, data):
--- a/Admin/website/css/isabelle_screen.css	Wed Apr 05 12:47:38 2006 +0200
+++ b/Admin/website/css/isabelle_screen.css	Wed Apr 05 17:38:32 2006 +0200
@@ -136,4 +136,19 @@
     font-size: 8pt;
     font-style: italics;
     padding: 0pt 12pt 0pt 0pt;
-}
\ No newline at end of file
+}
+
+/* people list */
+dl.people dt {
+    background-color: #EEEEEE;
+    padding: 2px;
+    margin-top: 8px;
+    height: 50px;
+}
+
+dl.people dd img {
+    float: right;
+    position: relative;
+    margin-right: 3px;
+    top: -52px;
+}