aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight
diff options
context:
space:
mode:
Diffstat (limited to 'exportclight')
-rw-r--r--exportclight/ExportClight.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 321ed8c9..4a85b591 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -514,6 +514,7 @@ let print_clightgen_info p sourcefile normalized =
fprintf p "@ Definition version := %S." Version.version;
fprintf p "@ Definition build_number := %S." Version.buildnr;
fprintf p "@ Definition build_tag := %S." Version.tag;
+ fprintf p "@ Definition build_branch := %S." Version.branch;
fprintf p "@ Definition arch := %S." Configuration.arch;
fprintf p "@ Definition model := %S." Configuration.model;
fprintf p "@ Definition abi := %S." Configuration.abi;