Commit db9ccd3d authored by Guillaume Melquiond's avatar Guillaume Melquiond

Do not reduce the font size for HTML documentation. Avoid long lines.

parent 34c0e42f
......@@ -18,14 +18,22 @@ installed provers is stored in the file
\texttt{provers-detection-data.conf} typically located in directory
\verb|/usr/local/share/why3| after installation. The contents of this
file is reproduced below.
{\footnotesize\lstinputlisting{../share/provers-detection-data.conf}}
%BEGIN LATEX
{\footnotesize
%END LATEX
\lstinputlisting{../share/provers-detection-data.conf}
%BEGIN LATEX
}
%END LATEX
\section{The \texttt{why3.conf} configuration file}
\label{sec:whyconffile}
\index{why3.conf@\texttt{why3.conf}}\index{configuration file}
\begin{figure}[p]
%BEGIN LATEX
{\footnotesize
%END LATEX
\begin{verbatim}
[main]
loadpath = "/usr/local/share/why3/theories"
......@@ -80,7 +88,9 @@ version = "0.93.1"
command = "coqide -I %l/coq-tactic -R %l/coq Why3 %f"
name = "CoqIDE"
\end{verbatim}
%BEGIN LATEX
}
%END LATEX
\caption{Sample why3.conf file}
\label{fig:why3conf}
\end{figure}
......
......@@ -289,7 +289,9 @@ exec = "iprover"
version_switch = " | grep iProver"
version_regexp = "iProver v\\([^ \n\t]+\\)"
version_ok = "0.8.1"
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e --fof true --out_options none --time_out_virtual %t --clausifier /usr/bin/env --clausifier_options \"eprover --cnf --tstp-format \" %f"
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e --fof true --out_options none \
--time_out_virtual %t --clausifier /usr/bin/env --clausifier_options \
\"eprover --cnf --tstp-format \" %f"
driver = "drivers/iprover.drv"
[ITP coq]
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment