added PRINT_COMMAND setting
authorwenzelm
Sun Jun 13 15:28:46 2004 +0200 (2004-06-13)
changeset 149333fd8c03e3ee6
parent 14932 df56e644da8f
child 14934 bf9f525d4821
added PRINT_COMMAND setting
doc-src/System/basics.tex
etc/settings
     1.1 --- a/doc-src/System/basics.tex	Sun Jun 13 15:28:30 2004 +0200
     1.2 +++ b/doc-src/System/basics.tex	Sun Jun 13 15:28:46 2004 +0200
     1.3 @@ -189,6 +189,9 @@
     1.4  \item[\settdx{DVI_VIEWER}] specifies the command to be used for displaying
     1.5    \texttt{dvi} files.
     1.6    
     1.7 +\item[\settdx{PRINT_COMMAND}] specifies the standard printer spool command,
     1.8 +  which is expected to accept PS files.
     1.9 +  
    1.10  \item[\settdx{ISABELLE_TMP_PREFIX}*] is the prefix from which any running
    1.11    \texttt{isabelle} process derives an individual directory for temporary
    1.12    files.  The default is somewhere in \texttt{/tmp}.
     2.1 --- a/etc/settings	Sun Jun 13 15:28:30 2004 +0200
     2.2 +++ b/etc/settings	Sun Jun 13 15:28:46 2004 +0200
     2.3 @@ -153,6 +153,9 @@
     2.4  #DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10"
     2.5  #DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9"
     2.6  
     2.7 +#Printer spool command for PS files
     2.8 +PRINT_COMMAND=lp
     2.9 +
    2.10  
    2.11  ###
    2.12  ### Interfaces