The lectures script is actually a bash script

The `pushd` and `popd` commands are bash commands. Expecting them
while being executed by /bin/sh does not make any sense. Indeed,
some linux distributions symlink /bin/sh to bash, but this is not
a good idea.

The lectures script fails on all standard distros such as Ubuntu
which is used for running the courses' sites.

script/lectures

@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 
 if [ -z "$REPOSITORY" -o -z "$BRANCH" ]; then
   echo "REPOSITORY and BRANCH should be set to a Git repository and a branch name"