blob: 2874456bc182c46a617bdb2801dc4f04647fc2a5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
#!/usr/bin/awk
#
BEGIN {
in_generate = 0;
in_verbatim = 0;
return_val = 1;
}
/^% GENERATE: *[a-z0-9A-Z_\.\-]+ *$/ && $3 == exname {
in_generate = 1;
return_val = 0;
next;
}
/^% END GENERATE$/ {
in_generate = 0;
next;
}
in_generate && /\\begin\{verbatim\}/ {
in_generate = 0;
in_verbatim = 1;
next;
}
in_verbatim && /\\end\{verbatim\}/ {
in_generate = 1;
in_verbatim = 0;
next;
}
in_generate && /^%/ {
print substr( $0, 2 );
}
in_verbatim {
print $0;
}
END { exit return_val; }
|