Merge branch 'master' of github.com:dbosk/introtools

adm/gits/datintro-setup.nw

@@ -110,6 +110,11 @@ for round in ${COURSE_CODE_ORG}; do
 
   users=$(mktemp)
   extract_users ${canvas_id} > ${users}
+  if [[ ! -s ${users} ]]; then
+    rm $users
+    continue
+  fi
+
   add_to_org ${gits_id} ${users}
   rm $users
 done

modules/git/grading/grade.sh.nw

@@ -103,6 +103,9 @@ grade_students() {
     local github=$(echo $course | cut -f 2 -d :)
 
     local students_w_times=$(students_with_grading_time "$canvas" "$assignm")
+    if [[ -z "$students_w_times" ]]; then
+      continue
+    fi
 
     local repos=$(clone_repos $github $(echo "$students_w_times" | cut -f 1))
 

modules/latex/grading/grade.sh.nw

@@ -188,6 +188,9 @@ grade_students() {
     local github=$(echo $course | cut -f 2 -d :)
 
     local students_w_times=$(students_with_grading_time "$canvas" "$assignm")
+    if [[ -z "$students_w_times" ]]; then
+      continue
+    fi
 
     local repos=$(clone_repos $github $(echo "$students_w_times" | cut -f 1))
 

modules/ssh/guide.md

@@ -41,13 +41,15 @@ also have a command-line interface, it's not compatible with a UNIX-like
 interface. If you run Windows 10, just go ahead and install Windows Subsystem 
 for Linux (WSL) to run Ubuntu in Windows. There are various guides:
 
+  - [Installing WSL2 on Windows][wsl2install] (FeedbackFruits, recommended)
   - [Microsoft's installation guide][ms-wsl] 
   - [Ubuntu's installation guide][ubuntu-wsl]
   - [omg!ubuntu!'s guide][WSL2]
   - [How-to-geek's guide][WSL]
 
 Pick your favourite!
 
+[wsl2install]: https://eu.feedbackfruits.com/courses/activity-course/0ccfb0cc-3274-470f-9def-0ddec7bd1c73
 [ms-wsl]: https://aka.ms/wsl2-install
 [ubuntu-wsl]: https://ubuntu.com/tutorials/ubuntu-on-windows#1-overview
 [WSL]: https://www.howtogeek.com/249966/how-to-install-and-use-the-linux-bash-shell-on-windows-10/