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

4 files changed, 4 insertions, 35 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 621f8acf1..51ee50300 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 4b448ad0b..51fe979f5 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"
diff --git a/ide/FAQ b/ide/FAQ
index 2079ef6ce..39dc095e4 100644
--- a/ide/FAQ
+++ b/ide/FAQ
@@ -49,21 +49,15 @@ R5)-First solution : type "<CONTROL><SHIFT>2200" to enter a forall in the script
 	Further symbols can be bound on higher Fxx keys or on even on other keys you
 	do not need .
 
-Q6) How to build a custom CoqIde with user ml code?
-R6) Use 
-	coqmktop -ide -byte m1.cmo...mi.cmo
-    or 
-	coqmktop -ide -opt m1.cmx...mi.cmx
-
-Q7) How to customize the shortcuts for menus?
-R7) Two solutions are offered:
+Q6) How to customize the shortcuts for menus?
+R6) Two solutions are offered:
   - Edit $HOME/.coqide.keys by hand or
   - Add "gtk-can-change-accels = 1" in your .coqide-gtk2rc file. Then
     from CoqIde, you may select a menu entry and press the desired 
     shortcut. 
 
-Q8) What encoding should I use? What is this \x{iiii} in my file?
-R8) The encoding option is related to the way files are saved. 
+Q7) What encoding should I use? What is this \x{iiii} in my file?
+R7) The encoding option is related to the way files are saved.
  Keep it as UTF-8 until it becomes important for you to exchange files 
  with non UTF-8 aware applications.
  If you choose something else than UTF-8, then missing characters will 
diff --git a/man/coqmktop.1 b/man/coqmktop.1
index 1b9c9e2a1..cae9f1e84 100644
--- a/man/coqmktop.1
+++ b/man/coqmktop.1
@@ -54,10 +54,6 @@ Build Coq on a ocaml toplevel (incompatible with
 Build a toplevel for SearchIsos
 
 .TP
-.B \-ide
-Build a toplevel for the Coq IDE
-
-.TP
 .BI \-R \ dir
 Specify recursively directories for Ocaml