doc-src/IsarOverview/Makefile
changeset 47333 8204b1023537
parent 47332 360e080fd13e
child 47334 4708384e759d
equal deleted inserted replaced
47332:360e080fd13e 47333:8204b1023537
     1 
       
     2 ## targets
       
     3 
       
     4 default: dvi
       
     5 
       
     6 ## dependencies
       
     7 
       
     8 dvi:
       
     9 	cd Isar/document; make dvi
       
    10 
       
    11 pdf:
       
    12 	cd Isar/document; make pdf
       
    13 
       
    14 clean:
       
    15 	cd Isar/document; make clean
       
    16 
       
    17 mrproper:
       
    18 	rm -f *.pdf *.dvi
       
    19 	cd Isar/document; make mrproper