+++ /dev/null
-#! /usr/bin/awk -f
-
-# Warning: this may use gnu-awk features
-
-# Program to create ascii from info;
-# Missing: table of contents
-
-# skip
-
-BEGIN {NODELINE=0; NODE=0; KEEP=1; printf "\n\n"}
-
-
-/^\037$/ { NODELINE=1; NODE=NODE+1; KEEP=1; next}
-
-NODE==1 { next }
-
-NODELINE==1 {
- NODELINE=2;
- sub("^.*Node: ","*Node: ");
- sub(",.*$","");
- printf "\n\n\n%s",$0;
-#print
- next;
- }
-
-NODELINE { NODELINE=NODELINE+1 }
-
-NODELINE==4 { printf "\t\t\t\t"; }
-NODELINE==5 { printf "\t\t\t\t"; NODELINE=0}
-
-
-/^\* Menu:$/ { KEEP=0 }
-
-
-
-KEEP==0 { next }
-
-{ print }