adjusted navigation width
authorhaftmann
Sat, 04 Jun 2005 21:49:30 +0200
changeset 16241 bf058cdf6841
parent 16240 95cc0e8f8a17
child 16242 f0d154b21b86
adjusted navigation width
Admin/website/TODO
Admin/website/build/pypager.py
Admin/website/dist/css/isabelle_screen.css
Admin/website/faq.html
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/TODO	Sat Jun 04 21:49:30 2005 +0200
@@ -0,0 +1,11 @@
+For the next release:
+
+- integrate into makedist (Florian), deploy on Munich site
+
+In the mid-time:
+
+-
+
+Visionary:
+
+-
\ No newline at end of file
--- a/Admin/website/build/pypager.py	Sat Jun 04 21:43:55 2005 +0200
+++ b/Admin/website/build/pypager.py	Sat Jun 04 21:49:30 2005 +0200
@@ -350,8 +350,6 @@
 
     def processingInstruction(self, target, data):
 
-        print '*', target
-        print '*', data
         self.closeLastStart()
         self.flushCharacterBuffer()
         func = getattr(self._func, target)
--- a/Admin/website/dist/css/isabelle_screen.css	Sat Jun 04 21:43:55 2005 +0200
+++ b/Admin/website/dist/css/isabelle_screen.css	Sat Jun 04 21:49:30 2005 +0200
@@ -65,7 +65,7 @@
     bottom: 4px;
     padding: 0.5em 0.5em;
     float: left;
-    width: 15ex;
+    width: 17ex;
     background-color: #FFFFFF;
     border-top: 2px solid #0000A0;
     border-bottom: 2px solid #0000A0;
--- a/Admin/website/faq.html	Sat Jun 04 21:43:55 2005 +0200
+++ b/Admin/website/faq.html	Sat Jun 04 21:49:30 2005 +0200
@@ -193,7 +193,7 @@
     
       <p>Alternatively you can set <tt class="shellcmd">LC_CTYPE</tt> or
       <tt class="shellcmd">LANG</tt> inside a file <tt class="shellcmd">~/.i18n</tt>, which
-      will be read by the shell. This will affect all applications, though.
+      will be read by the shell. This will affect all applications, though.</p>
       
       <p>Suggestions for a better workaround inside Emacs would be welcomed;</p>