diff --git a/doc/README.md b/doc/README.md index e75983f2b..4669eb5eb 100644 --- a/doc/README.md +++ b/doc/README.md @@ -14,7 +14,10 @@ Where do I start? The documentation is available at . -It can also be generated from the sources and browsed locally using any web +The online documentation generation is triggered each time new code is pushed to the master branch of the lambdapi repository on Github. +To this end, make sure the `.readthedocs.yaml` file is placed in the top-most directory of the Lambdapi repository and contains the well-suited configuration instructions as described in the [readthedocs documentation](https://docs.readthedocs.io/en/stable/config-file/index.html). + +The Lamdbapi user manual can also be generated from the sources and browsed locally using any web browser. To generate the documentation, [Sphinx](https://www.sphinx-doc.org/) @@ -26,9 +29,9 @@ sudo apt install python3-pip pip install -U sphinx sphinx_rtd_theme ``` -Change to directory `docs/` from the root of the sources -and use `make html` to generate `html` files into `docs/_build/html`. -The entry point of the documentation is `docs/_build/html/index.html`. +Change to directory `doc/` from the root of the sources +and use `make html` to generate `html` files into `doc/_build/html`. +The entry point of the documentation is `doc/_build/html/index.html`. How do I contribute? -------------------- diff --git a/editors/vscode/INSTALL.md b/editors/vscode/INSTALL.md index db24c4482..159e6d5db 100644 --- a/editors/vscode/INSTALL.md +++ b/editors/vscode/INSTALL.md @@ -22,6 +22,15 @@ export PATH=$node_dir:$PATH export NODE_PATH=$node_dir/lib/node_modules:$NODE_PATH ``` +Please note that adding nodejs to the `$PATH` by executing the `export` commands from the terminal will make it work only in the terminal where these commands have been run. + +Thus, you need to re-execute them each time you work from a new terminal. +If you intend to do this often, it is recomanded to add the two `export` commands to your `~/.bashrc` or `~/.profile` files and then apply changes with : + ```bash + source ~/.bashrc + source ~/.profile + ``` + - install dependencies: ```bash