doc: somehow wsl2.md was created so the page on https://leanprover.github.io/lean4/doc/make/wsl2.html is empty. This fixes that.

doc/SUMMARY.md

@@ -61,7 +61,7 @@
   - [Ubuntu Setup](./make/ubuntu-16.04.md)
   - [macOS Setup](./make/osx-10.9.md)
   - [Windows MSYS2 Setup](./make/msys2.md)
-  - [Windows with WSL](./make/wsl2.md)
+  - [Windows with WSL](./make/wsl.md)
   - [Nix Setup (*Experimental*)](./make/nix.md)
 - [Unit Testing](./dev/testing.md)
 - [Building This Manual](./dev/mdbook.md)

doc/dev/index.md

@@ -4,7 +4,7 @@
   - [Ubuntu Setup](../make/ubuntu-16.04.md)
   - [macOS Setup](../make/osx-10.9.md)
   - [Windows MSYS2 Setup](../make/msys2.md)
-  - [Windows with WSL](../make/wsl2.md)
+  - [Windows with WSL](../make/wsl.md)
   - [Nix Setup (*Experimental*)](../make/nix.md)
 - [Unit Testing](./testing.md)
 - [Building This Manual](./mdbook.md)

doc/make/wsl.md

@@ -27,20 +27,18 @@ into the WSL using: `Install in WSL: Ubuntu`
 Type `Ctrl+Shift+P` and select `Remote-WSL: Open Folder in WSL...` to
 open a folder containing your hello world lean package.
 
-When everything is working you should see this:
+When everything is working you should see something like this with a
+functioning infoview, syntax coloring and tooltips:
 
 ![screenshot](../images/code-wsl.png)
 
-with a functioning infoview, syntax coloring and tooltips.
 
 ## Troubleshooting
 
-**Connection to server is erroring. Shutting down server.**
+**lean4: Could not find Lean version by running 'lean --version'.**
 
-If your `leanpkg` has a `build` folder try deleting it.  Lean .olean
-binaries are not cross platform so if the binaries were copied from a
-different platform they need to be deleted so that the new build is
-created for your platform.
+Check that the `lean` program is available in your PATH in your WSL
+environment.
 
 **Logs are showing up with a windows file path**
 

doc/make/wsl2.md

@@ -1 +0,0 @@
-# Windows with WSL