# HG changeset patch
# User wenzelm
# Date 903971638 -7200
# Node ID 8521cd8b0a407b64ae4c21ba231246d355ffaac1
# Parent  f8bd38d9f8f32856ff488781b6bbb56beebec2c6
emacs local vars;
isatool install;

diff -r f8bd38d9f8f3 -r 8521cd8b0a40 doc-src/System/misc.tex
--- a/doc-src/System/misc.tex	Mon Aug 24 17:13:26 1998 +0200
+++ b/doc-src/System/misc.tex	Mon Aug 24 17:13:58 1998 +0200
@@ -46,7 +46,7 @@
 of the files are renamed to have the suffix~\verb'~~'.
 
 
-\section{Get logic images --- \texttt{isatool findlogics}}
+\section{Getting logic images --- \texttt{isatool findlogics}}
 
 The \tooldx{findlogics} utility traverses all directories specified in
 \texttt{ISABELLE_PATH}, looking for Isabelle logic images. Its usage
@@ -113,6 +113,35 @@
 \texttt{ISABELLE_PATH} (and also of \texttt{ISABELLE_OUTPUT}).
 
 
+\section{Installing Isabelle binaries with absolute references -- \texttt{isatool install}}
+\label{sec:tool-install}
+
+Usually, the Isabelle binaries (\texttt{isabelle}, \texttt{isatool}
+etc.) are just run from their location within the distribution
+directory, probably indirectly by the shell through its \texttt{PATH}.
+In some cases, though, another more traditional installation scheme
+might be preferably where executables are put into some global system
+directory (like \texttt{/usr/local/bin}).
+
+Doing a plain copy of the Isabelle executables just would not work,
+though.  One should use the \tooldx{install} utility instead:
+\begin{ttbox}
+Usage: install DIR
+
+  Install binaries in directory DIR with absolute references to
+  \$ISABELLE_HOME/bin (non-movable).
+\end{ttbox}
+
+The generated executables contain absolute references to
+\texttt{ISABELLE_HOME}, as figured out by the \texttt{isatool}
+invocation.  While the scripts themselves may be relocated afterwards,
+they would cease working if the referenced Isabelle distribution is
+moved.  This is an example use of \texttt{install}:
+\begin{ttbox}
+  isatool install /usr/local/bin
+\end{ttbox}
+
+
 \section{Isabelle's version of make --- \texttt{isatool make}}
 
 The Isabelle \tooldx{make} utility is a very simple wrapper for
@@ -225,3 +254,8 @@
 object-logics as a model for your own developements.  For example, see
 \texttt{src/FOL/IsaMakefile}.
 
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "system"
+%%% End: