From 1a52f581eb9cc52e5c1862c7e73253016109e1fc Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Fri, 23 Apr 2021 18:40:56 +0200
Subject: Remove `-version-file` option from option summary

The `-version-file` option was removed in commit 600803cae, but remained
in the option summary, as reported in #386.
---
 driver/CommonOptions.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'driver')

diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml
index e8a6941c..a816dd41 100644
--- a/driver/CommonOptions.ml
+++ b/driver/CommonOptions.ml
@@ -77,7 +77,6 @@ let general_help =
   -v             Print external commands before invoking them
   -timings       Show the time spent in various compiler passes
   -version       Print the version string and exit
-  -version-file <file> Print version inforation to <file> and exit
   -target <value> Generate code for the given target
   -conf <file>   Read configuration from file
   @<file>        Read command line options from <file>
-- 
cgit