From 0d727561aafcac28d036cddcb611e01109eca5dc Mon Sep 17 00:00:00 2001
From: pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 1 Sep 2011 09:51:17 +0000
Subject: same_file in Minilib

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14439 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/ideutils.mli | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'ide/ideutils.mli')

diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index fe8936877..23b31e4ae 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -67,13 +67,6 @@ val set_location : (string -> unit) ref
 
 val pbar : GRange.progress_bar
 
-
-(*
-  checks if two file names refer to the same (existing) file
-*)
-
-val same_file : string -> string -> bool
-
 (*
   returns an absolute filename equivalent to given filename
 *)
-- 
cgit v1.2.3