Skip to content

Commit

Permalink
clarify source tree sentence in 146
Browse files Browse the repository at this point in the history
  • Loading branch information
christinerose authored Jul 31, 2024
1 parent 80ba011 commit 7d858bd
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion doc/driver.mld
Original file line number Diff line number Diff line change
Expand Up @@ -140,7 +140,7 @@ directory.
[odoc] supports compiling {i implementations}. This can be useful to render source
code, generate links from and to source code, and count occurrences of
identifiers. The [compile-src] command takes a source-tree parent file and a
source path, which has to be in the source tree.
source path that has to be in the source tree.

Linking a file with [odoc] requires the input file and a list of include paths. As
for compile, we will hard-code the include path.
Expand Down

0 comments on commit 7d858bd

Please sign in to comment.