mathlib

f8206717 - ci(gitpod): do not rerun get-cache if a workspace is reloaded (#13949)

ci(gitpod): do not rerun get-cache if a workspace is reloaded (#13949) Instead, only run it at workspace start. This prevents it clobbering local builds created with `lean --make src` or similar. I have no idea why the `. /home/gitpod/.profile` line is there, so I've left it to run in the same phase as before.