+void PrintDbgSpanList (FILE* F, const ObjData* O, const unsigned* List)
+/* Output a string ",span=x[+y...]" for the given list. If the list is empty
+** or NULL, output nothing. This is a helper function for other modules to
+** print a list of spans read by ReadSpanList to the debug info file.
+*/
+{
+ if (List && *List) {
+ unsigned I;
+ const char* Format = ",span=%u";
+ for (I = 0; I < *List; ++I) {
+ fprintf (F, Format, O->SpanBaseId + List[I+1]);
+ Format = "+%u";
+ }
+ }
+}
+
+
+