phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update running_locally.md

Browse Source
This commit is contained in:
Pietro Monticone
2023-10-26 17:19:44 +02:00
parent d3a450f5b1
commit c4dc48292a
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
doc/running_locally.md
+1 -1
View File
@@ -15,7 +15,7 @@ The recommended option is "VSCode Dev containers" but you may choose any option
1. **Install Docker and Dev Containers** *(once)*:<br/>
See [official instructions](https://code.visualstudio.com/docs/devcontainers/containers#_getting-started).
Explicitely this means:
Explicitly this means:
* Install docker engine if you have not yet: [Instructions](https://docs.docker.com/engine/install/).
I followed the "Server" instructions for linux.
* Note that on Linux you need to add your user to the `docker` group