diff options
Diffstat (limited to 'docs/manual/external-toolchain.txt')
| -rw-r--r-- | docs/manual/external-toolchain.txt | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/docs/manual/external-toolchain.txt b/docs/manual/external-toolchain.txt index 62eb0a386..b33737609 100644 --- a/docs/manual/external-toolchain.txt +++ b/docs/manual/external-toolchain.txt @@ -1,6 +1,8 @@ -Using an external toolchain -=========================== +// -*- mode:doc -*- ; + [[external-toolchain]] +Using an external toolchain +~~~~~~~~~~~~~~~~~~~~~~~~~~~ Using an already existing toolchain is useful for different reasons: |