-
Robert Schmidt authored
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.
019778e9