cmd-interrupt.exp revision 1.2
11.1Srillig> cmd-interrupt-ordinary 21.2Srilligmake: *** cmd-interrupt-ordinary removed 31.2Srilliginterrupt-ordinary: ok 41.1Srillig> cmd-interrupt-phony 51.2Srilligmake: *** cmd-interrupt-phony removed 61.2Srilliginterrupt-phony: ok 71.2Srillig> cmd-interrupt-precious 81.2Srilliginterrupt-precious: ok 91.1Srilligexit status 0 10