search

replicate / codespaces

Internal scripts and tools to make Codespaces work better
6 stars 3 forks source link

handle case where docker.pid doesn't exist #7

Closed zeke closed 1 year ago

zeke commented 1 year ago

Once upon a time, GitHub changed something in the Codespaces env and we had to update our script to rm docker.pid. (See https://github.com/replicate/codespaces/pull/5)

Today, it seems that the env has changed again, and docker.pid is no longer around. This PR updates the script to delete the file if it exists, but not blow up if the file doesn't exist.

zeke commented 1 year ago

Shipping this but please still review!