aboutsummaryrefslogtreecommitdiffhomepage
path: root/man
diff options
context:
space:
mode:
authorGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2013-12-20 16:59:59 +0100
committerGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2013-12-20 17:27:20 +0100
commita665fd808b7fdaa11f84b35a87e0b8066cce1eda (patch)
tree2b4d5585bdb4b258fdad6f08af5b73bb9408e4a5 /man
parentca1305a0187653edcf63e46b84c65130ac78d117 (diff)
Coqdep always uses / as dir_sep
Diffstat (limited to 'man')
-rw-r--r--man/coqdep.14
1 files changed, 0 insertions, 4 deletions
diff --git a/man/coqdep.1 b/man/coqdep.1
index e9e0dd3e3..5a6cd609e 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -78,10 +78,6 @@ of each Coq file given as argument and complete (if needed)
the list of Caml modules. The new command is printed on
the standard output. No dependency is computed with this option.
.TP
-.BI \-slash
-Prints paths using a slash instead of the OS specific separator. This
-option is useful when developping under Cygwin.
-.TP
.BI \-I \ directory
The files .v .ml .mli of the directory
.IR directory \&