+
+/* For print media. */
+@media print {
+ /* Move the body up (no top menu anymore). */
+ body { margin-top: 4em; }
+
+ /* Hide the navigation. */
+ div#search_div { display: none; }
+ ul#topmenu { display: none; }
+ div#menu_div { display: none; }
+ p.edit_link { display: none; }
+
+ /* Display the target of external links. */
+ a.external {
+ background: none;
+ padding-right: 0px;
+ }
+ a.external:after {
+ content: " [" attr(href) "]";
+ }
+ a.mailto:after {
+ background: none;
+ padding-right: 0px;
+ }
+ a.mailto:after {
+ content: " [" attr(href) "]";
+ }
+}
\ No newline at end of file