lib/scripts/pic2png_eps.py

   1 #!/usr/bin/python
   2 # This script converts a raster format picture into a PNG and EPS file
   3
   4 import sys
   5 import os
   6
   7 if len(sys.argv) > 2:
   8         pars = sys.argv[2]
   9
  10 pid = os.fork()
  11 if pid == 0:
  12         os.execvp("convert", ["convert", pars, sys.argv[1], os.path.splitext(sys.argv[1])[0] + ".eps"])
  13         print "convert did not work"
  14         os.exit(1)
  15 os.wait()
  16
  17 pid = os.fork()
  18 if pid == 0:
  19         os.execvp("convert", ["convert", pars, sys.argv[1], os.path.splitext(sys.argv[1])[0] + ".png"])
  20         print "convert did not work second time"
  21         os.exit(1)
  22 os.wait()