diff --git a/Documentation/docinfo.html b/Documentation/docinfo.html
new file mode 100644
index 00000000000000..fb3560eb92b4ee
--- /dev/null
+++ b/Documentation/docinfo.html
@@ -0,0 +1,5 @@
+<style>
+pre>code {
+   display: inline;
+}
+</style>