File tree Expand file tree Collapse file tree
Src/Scripts/TutorialsChecker Expand file tree Collapse file tree Original file line number Diff line number Diff line change 11#! /bin/bash
22
3- SCHEDULES=25000
3+ DEFAULT_SCHEDULES=25000
4+ RAFT_SCHEDULES=1000
45
56cd $1
67
@@ -16,10 +17,19 @@ for folder in $folders; do
1617 # If so, change into folder and compile
1718 if [ -n " $pprojFiles " ]; then
1819 cd $folder
19-
20- echo " ------------------------------------------------------"
21- echo " Checking $folder !"
22- echo " ------------------------------------------------------"
20+
21+ # Set schedules based on folder name
22+ if [[ " $folder " == " 6_Raft/" ]]; then
23+ SCHEDULES=$RAFT_SCHEDULES
24+ echo " ------------------------------------------------------"
25+ echo " Checking $folder with $SCHEDULES iterations (reduced)!"
26+ echo " ------------------------------------------------------"
27+ else
28+ SCHEDULES=$DEFAULT_SCHEDULES
29+ echo " ------------------------------------------------------"
30+ echo " Checking $folder with $SCHEDULES iterations!"
31+ echo " ------------------------------------------------------"
32+ fi
2333
2434 checkLog=" check.log"
2535 p check -i ${SCHEDULES} 2>&1 | tee ${checkLog}
You can’t perform that action at this time.
0 commit comments