Skip to content

Commit

Permalink
fix: DOCGEN_SOURCE -> DOCGEN_SRC to match code in README
Browse files Browse the repository at this point in the history
  • Loading branch information
jesse-michael-han authored and hargoniX committed Jan 8, 2024
1 parent d82d610 commit 29f7f43
Showing 1 changed file with 6 additions and 6 deletions.
12 changes: 6 additions & 6 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -52,19 +52,19 @@ out things that you intend to complete later.

## Source locations

Source locations default to guessing the Github repo for the library, but different different schemas can be used by setting the `DOCGEN_SOURCE` environment variable. For
Source locations default to guessing the Github repo for the library, but different different schemas can be used by setting the `DOCGEN_SRC` environment variable. For
example, one can use links that open the local source file in VSCode by running lake with:
```
DOCGEN_SOURCE="vscode" lake -R -Kenv=dev ...
DOCGEN_SRC="vscode" lake -R -Kenv=dev ...
```

The different options are:

* `DOCGEN_SOURCE="github"` infers the
* `DOCGEN_SRC="github"` infers the
Github project for each library and uses source links to the Github source view.
This is the default if `DOCGEN_SOURCE` is unset.
* `DOCGEN_SOURCE="file"` creates references to local file references.
* `DOCGEN_SOURCE="vscode"` creates [VSCode URLs](https://code.visualstudio.com/docs/editor/command-line#_opening-vs-code-with-urls) to local files.
This is the default if `DOCGEN_SRC` is unset.
* `DOCGEN_SRC="file"` creates references to local file references.
* `DOCGEN_SRC="vscode"` creates [VSCode URLs](https://code.visualstudio.com/docs/editor/command-line#_opening-vs-code-with-urls) to local files.

## How does `docs#Nat.add` from the Lean Zulip work?
If someone sends a message that contains `docs#Nat.add` on the Lean Zulip this will
Expand Down

0 comments on commit 29f7f43

Please sign in to comment.