diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/faq/FAQ.tex | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-ide.tex | 15 |
2 files changed, 0 insertions, 21 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 621f8acf17..51ee50300f 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -2415,12 +2415,6 @@ Glib.Utf8.from_unichar 0x2200;; do not need . \end{itemize} -\Question{How to build a custom {\CoqIde} with user ml code?} - Use - coqmktop -ide -byte m1.cmo...mi.cmo - or - coqmktop -ide -opt m1.cmx...mi.cmx - \Question{How to customize the shortcuts for menus?} Two solutions are offered: \begin{itemize} diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index 4b448ad0be..51fe979f56 100644 --- a/doc/refman/RefMan-ide.tex +++ b/doc/refman/RefMan-ide.tex @@ -299,21 +299,6 @@ each dot is an hexadecimal digit: the number between braces is the hexadecimal UNICODE index for the missing character. -\section{Building a custom \CoqIDE{} with user \textsc{ML} code} - -You can do this as described in Section~\ref{Coqmktop} for a -custom coq text toplevel, simply by adding -option \verb|-ide| to \verb|coqmktop|, that is something like -\begin{quote} -\texttt{coqmktop -ide -byte $m_1$.cmo \ldots{} $m_n$.cmo} -\end{quote} -or -\begin{quote} -\texttt{coqmktop -ide -opt $m_1$.cmx \ldots{} $m_n$.cmx} -\end{quote} - - - %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" |