diff options
| author | Emilio Jesus Gallego Arias | 2018-10-02 17:45:51 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-02 18:46:38 +0200 |
| commit | be640372098d01e8c99b60bdc648ec806b8a4b2c (patch) | |
| tree | ea3ef680686fb2e8ccde4cf6e79482380ac4a073 /doc | |
| parent | 24550259892e9e408b11359fa71b240083e7546f (diff) | |
[doc] Nits on utilities / toplevel building.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 5d300c3d6d..19995520bb 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -21,16 +21,16 @@ The most basic custom toplevel is built using: % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \ -package coq.toplevel \ - toplevel/coqtop\_bin.ml -o my\_toplevel.native + topbin/coqtop_bin.ml -o my_toplevel.native -For example, to statically link |L_tac|, you can just do: +For example, to statically link |Ltac|, you can just do: :: % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \ - -package coq.toplevel -package coq.ltac \ - toplevel/coqtop\_bin.ml -o my\_toplevel.native + -package coq.toplevel,coq.plugins.ltac \ + topbin/coqtop_bin.ml -o my_toplevel.native and similarly for other plugins. |