New command line option: --xml-user-comment=XMLTEXT, which allows
copying of arbitrary bits of XML text to the XML output.
git-svn-id: svn://svn.valgrind.org/valgrind/trunk@4186 a5019735-40e9-0310-863c-91ae7b9d1cf9
diff --git a/include/pub_tool_options.h b/include/pub_tool_options.h
index e27e158..8266a3a 100644
--- a/include/pub_tool_options.h
+++ b/include/pub_tool_options.h
@@ -71,6 +71,10 @@
way. See vg_main.c and mc_main.c. */
extern Bool VG_(clo_xml);
+/* An arbitrary user-supplied string which is copied into the
+ XML output, in between <usercomment> tags. */
+extern HChar* VG_(clo_xml_user_comment);
+
/* Call this if a recognised option was bad for some reason.
Note: don't use it just because an option was unrecognised -- return 'False'
from VG_(tdict).tool_process_cmd_line_option) to indicate that. */