Use dev drive for target

which is the most write-heavy part.

The read to the workspace can be cached as it is really small

Signed-off-by: Jiahao XU <30436523+NobodyXu@users.noreply.github.com>
This commit is contained in:
Jiahao XU 2024-08-25 20:48:16 +10:00 committed by GitHub
parent 8fcaf36eaf
commit e55c4282cb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -24,12 +24,9 @@ runs:
- uses: samypr100/setup-dev-drive@v3
if: runner.os == 'Windows'
with:
workspace-copy: true
drive-size: 6GB
mount-path: ${{ github.workspace }}/target
drive-size: 5GB
drive-type: Fixed
env-mapping: |
CARGO_HOME,{{ DEV_DRIVE }}/.cargo
RUSTUP_HOME,{{ DEV_DRIVE }}/.rustup
- name: Add just to tools to install
run: echo "tools=just" >>"$GITHUB_ENV"