equal
deleted
inserted
replaced
17 (******************************************************************) |
17 (******************************************************************) |
18 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
18 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
19 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
19 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
20 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
20 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
21 (******************************************************************) |
21 (******************************************************************) |
22 |
|
23 print_depth 0; |
|
24 |
22 |
25 (* |
23 (* |
26 This file is generated from the contents of ML-Yacc's lib directory. |
24 This file is generated from the contents of ML-Yacc's lib directory. |
27 ML-Yacc's COPYRIGHT-file contents follow: |
25 ML-Yacc's COPYRIGHT-file contents follow: |
28 |
26 |
46 $MLYACCDIR/lib/$FILE |
44 $MLYACCDIR/lib/$FILE |
47 done |
45 done |
48 |
46 |
49 cat <<EOF |
47 cat <<EOF |
50 ; |
48 ; |
51 print_depth 10; |
|
52 EOF |
49 EOF |
53 |
50 |
54 ) > ml_yacc_lib.ML |
51 ) > ml_yacc_lib.ML |