From 0866e2c63763fef5ad5e461de8ba19c5592c01a1 Mon Sep 17 00:00:00 2001
From: brutzman <brutzman@nps.edu>
Date: Mon, 14 Sep 2020 17:05:00 -0700
Subject: [PATCH] pre style background-color

---
 developers.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/developers.html b/developers.html
index 68e3cd9cb2..d699115e9b 100644
--- a/developers.html
+++ b/developers.html
@@ -2391,7 +2391,7 @@ netbeans_jdkhome="C:\Program Files\Java\jdk1.8.0_221"</pre>
           Example information for <i>conf/tomcat-users.xml</i> configuration file follows.
           Note that any username must also be configured in the Tomcat installation itself.
       </p>
-<pre>
+<pre style="background-color:lightgrey">
 &lt;role rolename="admin"/&gt;
 &lt;role rolename="admin-gui"/&gt;
 &lt;role rolename="admin-script"/&gt;
-- 
GitLab