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 import os.path
   7
   8 if len(sys.argv) > 2:
   9         pars = sys.argv[2]
  10
  11 pid = os.fork()
  12 if pid == 0:
  13         os.execvp("convert", ["convert", pars, sys.argv[1], os.path.splitext(sys.argv[1])[0] + ".eps"])
  14         print "convert did not work"
  15         os.exit(1)
  16 os.wait()
  17
  18 pid = os.fork()
  19 if pid == 0:
  20         os.execvp("convert", ["convert", pars, sys.argv[1], os.path.splitext(sys.argv[1])[0] + ".png"])
  21         print "convert did not work second time"
  22         os.exit(1)
  23 os.wait()