height            349 src/prt2pdf/prt2pdf.c   float height;
height            389 src/prt2pdf/prt2pdf.c   height = GLOBAL_SHADE_STEP * GLOBAL_LEAD_SIZE;
height            390 src/prt2pdf/prt2pdf.c   yyy1 = GLOBAL_PAGE_DEPTH - GLOBAL_PAGE_MARGIN_TOP - height - 0.22 * GLOBAL_FONT_SIZE;
height            394 src/prt2pdf/prt2pdf.c     yyy1 -= height; /* Shift the starting point down by one bar */
height            396 src/prt2pdf/prt2pdf.c   while (yyy1 >= (GLOBAL_PAGE_MARGIN_BOTTOM - height))
height            398 src/prt2pdf/prt2pdf.c       (void)fprintf (stdout, "%f %f %f %f re f\n", x1, yyy1, width, height);
height            399 src/prt2pdf/prt2pdf.c       yyy1 = yyy1 - step * height;