rs (run statistics) does not work
Created by: giannou
due to the renaming of log.txt to $JOBNAME.out in https://github.com/remindmodel/remind/commit/285f5c23dc3d79c4e89dd510778d0f20c93b1343
Created by: giannou
due to the renaming of log.txt to $JOBNAME.out in https://github.com/remindmodel/remind/commit/285f5c23dc3d79c4e89dd510778d0f20c93b1343