aboutsummaryrefslogtreecommitdiffstats
path: root/driver/CommonOptions.ml
diff options
context:
space:
mode:
authorChristoph Cullmann <cullmann@kde.org>2020-07-30 09:59:14 +0200
committerChristoph Cullmann <cullmann@kde.org>2020-07-30 10:00:26 +0200
commit6903cff15e6a66982513f5fe1511ed70eb781cbd (patch)
tree1fb3eb7172915eb4c4d6248b0990c9bb3494cfe2 /driver/CommonOptions.ml
parent338509aef7347fda5db4123d645bb52971fa8a91 (diff)
downloadcompcert-kvx-6903cff15e6a66982513f5fe1511ed70eb781cbd.tar.gz
compcert-kvx-6903cff15e6a66982513f5fe1511ed70eb781cbd.zip
Add missing comment for print_version_file_and_exit
Diffstat (limited to 'driver/CommonOptions.ml')
-rw-r--r--driver/CommonOptions.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml
index 5993c68d..cbc04a44 100644
--- a/driver/CommonOptions.ml
+++ b/driver/CommonOptions.ml
@@ -32,6 +32,7 @@ let version_file_string tool_name =
else
Printf.sprintf "The CompCert %s,\nversion %s\n" tool_name Version.version
+(* Print the version string to a file and exit the program *)
let print_version_file_and_exit tool_name file =
let oc = open_out_bin file in
output_string oc (version_file_string tool_name);