equal
deleted
inserted
replaced
119 val result = input (is, 999999); |
119 val result = input (is, 999999); |
120 in close_out os; |
120 in close_out os; |
121 close_in is; |
121 close_in is; |
122 result |
122 result |
123 end; |
123 end; |
|
124 |
|
125 |
|
126 |
|
127 val needs_filtered_use = true; |