#! /bin/bash
# Last edited on 2024-04-01 14:43:26 by stolfi

usage="$0 < INFILE.ps > OUTFILE.pdf"

#   -r600 -g6600x5100 \

gs \
  -sDEVICE=pdfwrite \
  -sOutputFile=- \
  -q \
  -dNOPAUSE \
  -dNOPLATFONTS \
  -dBATCH \
  -