diff options
| author | Duncan Coutts <duncan.coutts@worc.ox.ac.uk> | 2006-01-17 19:29:55 +0000 |
|---|---|---|
| committer | Duncan Coutts <duncan.coutts@worc.ox.ac.uk> | 2006-01-17 19:29:55 +0000 |
| commit | aa36c783045c5116b773ef5a4e843d916dbe6e3c (patch) | |
| tree | 9c7fc7f8e9015cf78dc691f9a943ead468a6b20c /html/plus.gif | |
| parent | 766cecdda0a834e2a50a6aaa36518ea6b4ac360c (diff) | |
Add a --wiki=URL flag to add a per-module link to a correspondng wiki page.
So each html page gets an extra link (placed next to the source code and
contents links) to a corresponding wiki page. The idea is to let readers
contribute their own notes, examples etc to the documentation.
Also slightly tidy up the code for the --source option.
Diffstat (limited to 'html/plus.gif')
0 files changed, 0 insertions, 0 deletions