Klaus-Peter schrieb:
- wofuer wird der Dokumentenname im Header eigentlich gebraucht?
Ich vermute, dass er beim Verschieben der Dateien behilflich sein soll. Vielleicht sollen wir auch das Maintenance unseres Servers automatisieren, dann wird ein Dokumentenname unersetzlich. Wenn sie nicht gebraucht wird, warum sollen wir sie einbauen?
und damit, muessen in den Dateien, wo keiner drin ist, welche eingebaut werden?
Das koennte man auch fuer die herkoemmlichen Seiten automatisch tun. Nur wenn die Autoren ihre lokale Kopien weiter bearbeiten, geht's schief.
- wenn Du schreibst: "falschen Dokumentennamen", ist der "Case sensitiv"?
Ja, wie alle Dateiennamen unter Unix. Ich habe das Skript ueberarbeitet, und einige Fehler darin korrigiert. Jetzt finde ich 813 HTML Dateien mit dem richtigen Dokumentennamen, 132 mit echten Fehlern, 147 mit Fehlern aber nur in dem Pathnamen, 53 mit verkuerztem Pathnamen, 433 ohne Dokumentennamen, und 41 ohne Header. Wenn es noch von Interesse ist, kann ich die Dateiennamen posten. -- =Jim Eggert EggertJ@LL.mit.edu