1 files changed, 0 insertions, 6 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}