• Robert Schmidt's avatar
    Simplify create_workspace.sh: remove unnecessary checkout · 019778e9
    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
create_workspace.sh 509 Bytes