diff --git a/repos/base/include/util/xml_generator.h b/repos/base/include/util/xml_generator.h index c8072fd9d9..7939943302 100644 --- a/repos/base/include/util/xml_generator.h +++ b/repos/base/include/util/xml_generator.h @@ -357,6 +357,12 @@ class Genode::Xml_generator attribute(name, static_cast(value)); } + void attribute(char const *name, double value) + { + String<64> buf(value); + _curr_node->insert_attribute(name, buf.string()); + } + /** * Append content to XML node *