diff options
Diffstat (limited to 'docs/CommandGuide/opt.html')
| -rw-r--r-- | docs/CommandGuide/opt.html | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/docs/CommandGuide/opt.html b/docs/CommandGuide/opt.html index 2e531a9202..75b93602e4 100644 --- a/docs/CommandGuide/opt.html +++ b/docs/CommandGuide/opt.html @@ -76,22 +76,6 @@ writes its output to the standard output. href="../ProgrammersManual.html#DEBUG">Programmer's Manual</a> for more information. <p> -<!-- - <li> -internalize-public-api-file <filename> - <br> - Preserve the symbol names listed in the file filename. - <p> - - <li> -internalize-public-api-list=<list> - <br> - Perserve the symbol names specified. - <p> ---> - - <li> -q - <br> - Quiet mode. Do not print messages on whether the program was modified. - <p> <li> -load <plugin> <br> |