publish (695B)
1 #!/usr/local/plan9/bin/rc 2 3 dir=$9fansweb 4 if (~ $#dir 0) { 5 dir=$home^/pub/9fans.github.io 6 9fansweb=$dir 7 } 8 9 root=$dir/plan9port 10 if (! test -d $root) { 11 echo $root does not exist >[1=2] 12 exit bad 13 } 14 15 rm -rf $root/man 16 cp -a ../man $root/man 17 mkdir -p $root/unix 18 cp unix.html $root/unix/index.html 19 cp main.html $root/index.html 20 cp ss.html $root/screenshots/index.html 21 @{cd ../unix/man && mk push} 22 @{cd ../unix && mk push} 23 24 rm -rf $root/../usr/local/plan9 25 mkdir -p $root/../usr/local/plan9 26 @{cd ..; git archive HEAD} | @{cd $root/../usr/local/plan9 && u tar xf -} 27 for(d in `{find $root/../usr/local/plan9 -type d}) { 28 9 rc ./mkdirlist $d `{echo $d | sed 's;.*/usr;/usr;'} >t1 && mv t1 $d/index.html 29 }