Robert Schmidt 019778e927 Simplify create_workspace.sh: remove unnecessary checkout ...

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.

2024-11-09 12:41:23 +01:00

..

create_workspace.sh

Simplify create_workspace.sh: remove unnecessary checkout

2024-11-09 12:41:23 +01:00