|
||||||||||
| PREV NEXT | FRAMES NO FRAMES | |||||||||
| Packages that use UnbufferredPushChannel | |
|---|---|
| at.dms.kjc.backendSupport | Package documentation for at.dms.kjc.backendSupport |
| Uses of UnbufferredPushChannel in at.dms.kjc.backendSupport |
|---|
| Methods in at.dms.kjc.backendSupport that return UnbufferredPushChannel | |
|---|---|
static UnbufferredPushChannel |
UnbufferredPushChannel.getChannel(Edge edge,
String pushName)
Make a new Channel or return an already-made channel. |
|
||||||||||
| PREV NEXT | FRAMES NO FRAMES | |||||||||