From bdeccec95e1d018ffb18af9209060a9806d0235a Mon Sep 17 00:00:00 2001
From: pboutill
Date: Fri, 25 May 2012 12:50:13 +0000
Subject: Bugs revealed by playing with contribs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15364 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/project_file.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index 87ddee081f..6ae5e08bed 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -54,7 +54,7 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
     process_cmd_line orig_dir (project_file,makefile,install,true) l r
   | "-impredicative-set" :: r ->
     Minilib.log "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.";
-    process_cmd_line orig_dir opts (Arg "-impredicative_set" :: l) r
+    process_cmd_line orig_dir opts (Arg "-impredicative-set" :: l) r
   | "-no-install" :: r ->
     Minilib.log "Option -no-install is deprecated. Use \"-install none\" instead";
     process_cmd_line orig_dir (project_file,makefile,NoInstall,opt) l r
-- 
cgit v1.2.3