equal
deleted
inserted
replaced
26 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
26 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
27 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
27 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
28 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
28 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
29 (******************************************************************) |
29 (******************************************************************) |
30 |
30 |
31 print_depth 0; |
|
32 |
|
33 EOF |
31 EOF |
34 |
32 |
35 for FILE in $FILES |
33 for FILE in $FILES |
36 do |
34 do |
37 echo |
35 echo |
49 sed 's/\(.*\)/s\/\\\\b\1\\\\b\/Metis_\1\/g;/'`" |
47 sed 's/\(.*\)/s\/\\\\b\1\\\\b\/Metis_\1\/g;/'`" |
50 done |
48 done |
51 |
49 |
52 cat <<EOF |
50 cat <<EOF |
53 ; |
51 ; |
54 print_depth 10; |
|
55 EOF |
52 EOF |
56 |
53 |
57 ) > metis.ML |
54 ) > metis.ML |