diff options
Diffstat (limited to 'docs/CommandGuide/opt.html')
| -rw-r--r-- | docs/CommandGuide/opt.html | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/docs/CommandGuide/opt.html b/docs/CommandGuide/opt.html index 91650d66e8..4bf67a49c2 100644 --- a/docs/CommandGuide/opt.html +++ b/docs/CommandGuide/opt.html @@ -53,6 +53,16 @@ writes its output to the standard output. Specify the output filename. <p> + <li> -dsa-track-integers + <br> + Track integers as potential pointers. + <p> + + <li> -profile-info-file <filename> + <br> + Specify the name of the file loaded by the -profile-loader option. + <p> + <li> -stats <br> Print statistics. |