1.1 --- a/doc-src/System/misc.tex	Mon Aug 24 17:13:26 1998 +0200
     1.2 +++ b/doc-src/System/misc.tex	Mon Aug 24 17:13:58 1998 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4  of the files are renamed to have the suffix~\verb'~~'.
     1.5  
     1.6  
     1.7 -\section{Get logic images --- \texttt{isatool findlogics}}
     1.8 +\section{Getting logic images --- \texttt{isatool findlogics}}
     1.9  
    1.10  The \tooldx{findlogics} utility traverses all directories specified in
    1.11  \texttt{ISABELLE_PATH}, looking for Isabelle logic images. Its usage
    1.12 @@ -113,6 +113,35 @@
    1.13  \texttt{ISABELLE_PATH} (and also of \texttt{ISABELLE_OUTPUT}).
    1.14  
    1.15  
    1.16 +\section{Installing Isabelle binaries with absolute references -- \texttt{isatool install}}
    1.17 +\label{sec:tool-install}
    1.18 +
    1.19 +Usually, the Isabelle binaries (\texttt{isabelle}, \texttt{isatool}
    1.20 +etc.) are just run from their location within the distribution
    1.21 +directory, probably indirectly by the shell through its \texttt{PATH}.
    1.22 +In some cases, though, another more traditional installation scheme
    1.23 +might be preferably where executables are put into some global system
    1.24 +directory (like \texttt{/usr/local/bin}).
    1.25 +
    1.26 +Doing a plain copy of the Isabelle executables just would not work,
    1.27 +though.  One should use the \tooldx{install} utility instead:
    1.28 +\begin{ttbox}
    1.29 +Usage: install DIR
    1.30 +
    1.31 +  Install binaries in directory DIR with absolute references to
    1.32 +  \$ISABELLE_HOME/bin (non-movable).
    1.33 +\end{ttbox}
    1.34 +
    1.35 +The generated executables contain absolute references to
    1.36 +\texttt{ISABELLE_HOME}, as figured out by the \texttt{isatool}
    1.37 +invocation.  While the scripts themselves may be relocated afterwards,
    1.38 +they would cease working if the referenced Isabelle distribution is
    1.39 +moved.  This is an example use of \texttt{install}:
    1.40 +\begin{ttbox}
    1.41 +  isatool install /usr/local/bin
    1.42 +\end{ttbox}
    1.43 +
    1.44 +
    1.45  \section{Isabelle's version of make --- \texttt{isatool make}}
    1.46  
    1.47  The Isabelle \tooldx{make} utility is a very simple wrapper for
    1.48 @@ -225,3 +254,8 @@
    1.49  object-logics as a model for your own developements.  For example, see
    1.50  \texttt{src/FOL/IsaMakefile}.
    1.51  
    1.52 +
    1.53 +%%% Local Variables: 
    1.54 +%%% mode: latex
    1.55 +%%% TeX-master: "system"
    1.56 +%%% End: