File diff 000000000000 → 000000000000
makedot.sh
Show inline comments
 
new file 100755
 
#!/bin/bash
 

	
 
DOTOPTS="-Nfontsize=15 -Tpdf"
 

	
 
dot recycling-noopt.dot $DOTOPTS > recycling-noopt.pdf 
 
dot recycling-opt.dot $DOTOPTS > recycling-opt.pdf 
 

	
 
dot identity-noopt.dot $DOTOPTS > identity-noopt.pdf 
 
dot identity-opt.dot $DOTOPTS > identity-opt.pdf 
 

	
 
dot pushdown-noopt.dot $DOTOPTS > pushdown-noopt.pdf 
 
dot pushdown-opt.dot $DOTOPTS > pushdown-opt.pdf 
 

	
 
dot parallel.dot $DOTOPTS > parallel-tree.pdf 
 

	
 
dot survey-noopt.dot $DOTOPTS > survey-noopt.pdf 
 
dot survey-opt.dot $DOTOPTS > survey-opt.pdf 
 

	
 

	
 
dot defer.dot $DOTOPTS > defer.pdf