create_workspace.sh used to check out develop by default. However, this
is unnecessary because the script later checks out a specific reference
(which can be a commit ID, which is not accepted by git clone, the
reason we don't check out during clone); the repository will simply be
empty in the beginning, which should not be a problem.
Further, it is problematic because we use this script for the build of
the L2sim proxy, and the repository does not have develop; thus, without
this modification, L2sim proxy build will always fail.
Robert Schmidt
019778e927