diff options
Diffstat (limited to '020run.cc')
| -rw-r--r-- | 020run.cc | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/020run.cc b/020run.cc index 0f196b82..c2a44019 100644 --- a/020run.cc +++ b/020run.cc @@ -96,6 +96,7 @@ void run_current_routine() //? cout << "DDD: " << current_instruction().to_string() << '\n'; //? 1 current_step_index() = instruction_counter+1; } + stop_running_current_routine:; } //: Some helpers. |