make use of the new progress bar monitor in interactive mode, while remaining with the logger MojoRascalMonitor in batch mode#19

Merged

jurgenvinju merged 2 commits intomainfrom progress-bars

May 13, 2024

+57-23

Commits on Apr 8, 2024

make use of the new progress bar monitor in interactive mode, while remaining with the logger MojoRascalMonitor in batch mode
jurgenvinju
committed
fixed startup race. the monitor should probably be a singleton
jurgenvinju
committed