From 6599e31f04b6e8980de72e9d3913b70c04b6698c Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 6 Jan 2016 15:08:08 +0100
Subject: Remove deprecated command-line options such as "-as".

---
 ide/project_file.ml4 | 1 -
 1 file changed, 1 deletion(-)

(limited to 'ide')

diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index f66fd31c20..081094e2b6 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -86,7 +86,6 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
     process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir, lp)) :: l) r
   | "-I" :: d :: r ->
     process_cmd_line orig_dir opts ((MLInclude (CUnix.correct_path d orig_dir)) :: l) r
-  | "-R" :: p :: "-as" :: lp :: r
   | "-R" :: p :: lp :: r ->
     process_cmd_line orig_dir opts (RInclude (CUnix.correct_path p orig_dir,lp) :: l) r
   | ("-Q"|"-R"|"-I"|"-custom"|"-extra"|"-extra-phony") :: _ ->
-- 
cgit v1.2.3