+/**
+ * printf the VCG color
+ */
+static void print_vcg_color(FILE *F, dumper_colors color) {
+ static const char *color_names[32] = {
+ "white", "blue", "red", "green",
+ "yellow", "magenta", "cyan", "darkgray",
+ "darkblue", "darkred", "darkgreen", "darkyellow",
+ "darkmagenta", "darkcyan", "gold", "lightgray",
+ "lightblue", "lightred", "lightgreen", "lightyellow",
+ "lightmagenta", "lightcyan", "lilac", "turquoise",
+ "aquamarine", "khaki", "purple", "yellowgreen",
+ "pink", "orange", "orchid", "black"
+ };
+
+ if (color != ird_color_default)
+ fprintf(F, "color:%s", color_names[color]);
+}
+