# HG changeset patch
# User wenzelm
# Date 1087133326 -7200
# Node ID 3fd8c03e3ee66cf81c9110ff8f2bebd2fe6b8dce
# Parent  df56e644da8f54213ce4dc44c7c7fa81e5459a6f
added PRINT_COMMAND setting

diff -r df56e644da8f -r 3fd8c03e3ee6 doc-src/System/basics.tex
--- a/doc-src/System/basics.tex	Sun Jun 13 15:28:30 2004 +0200
+++ b/doc-src/System/basics.tex	Sun Jun 13 15:28:46 2004 +0200
@@ -189,6 +189,9 @@
 \item[\settdx{DVI_VIEWER}] specifies the command to be used for displaying
   \texttt{dvi} files.
   
+\item[\settdx{PRINT_COMMAND}] specifies the standard printer spool command,
+  which is expected to accept PS files.
+  
 \item[\settdx{ISABELLE_TMP_PREFIX}*] is the prefix from which any running
   \texttt{isabelle} process derives an individual directory for temporary
   files.  The default is somewhere in \texttt{/tmp}.
diff -r df56e644da8f -r 3fd8c03e3ee6 etc/settings
--- a/etc/settings	Sun Jun 13 15:28:30 2004 +0200
+++ b/etc/settings	Sun Jun 13 15:28:46 2004 +0200
@@ -153,6 +153,9 @@
 #DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10"
 #DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9"
 
+#Printer spool command for PS files
+PRINT_COMMAND=lp
+
 
 ###
 ### Interfaces