[project @ 2003-07-15 13:28:27 by cjwatson]

[debbugs.git] / html / Developer.html.in

diff --git a/html/Developer.html.in b/html/Developer.html.in
index c512a7f9d0b1d04ce0ee359bde472eb9e0794abe..5dad8b9d7a7eceb2f589a2ec8ec81d29270c9058 100644 (file)
--- a/html/Developer.html.in
+++ b/html/Developer.html.in
@@ -84,6 +84,7 @@ the $gBug is submitted (see the
 <a href="Reporting.html#pseudoheader">instructions for reporting $gBugs</a>),
 or by using the <code>severity</code> command with the
 <a href="#requestserv">control request server</a>.
+Separate multiple tags with commas, spaces, or both.
 
 <p>The severity levels are: