From f661bda0849b0a3008e4dc1bba66addd0f84a571 Mon Sep 17 00:00:00 2001
From: glondu
Date: Tue, 11 Jan 2011 19:12:06 +0000
Subject: Remove references to -ide option of coqmktop

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13789 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-ide.tex | 15 ---------------
 1 file changed, 15 deletions(-)

(limited to 'doc/refman')

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"
-- 
cgit v1.2.3