equal
deleted
inserted
replaced
137 } |
137 } |
138 |
138 |
139 /* |
139 /* |
140 * Tell the OutputRecord that a finished message was |
140 * Tell the OutputRecord that a finished message was |
141 * contained either in this record or the one immeiately |
141 * contained either in this record or the one immeiately |
142 * preceeding it. We need to reliably pass back notifications |
142 * preceding it. We need to reliably pass back notifications |
143 * that a finish message occured. |
143 * that a finish message occurred. |
144 */ |
144 */ |
145 void setFinishedMsg() { |
145 void setFinishedMsg() { |
146 assert(socket == null); |
146 assert(socket == null); |
147 |
147 |
148 ((EngineOutputRecord)r).setFinishedMsg(); |
148 ((EngineOutputRecord)r).setFinishedMsg(); |