aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar Trevor Elliott <trevor@galois.com>2013-06-20 11:01:14 -0700
committerGravatar Trevor Elliott <trevor@galois.com>2013-06-20 11:01:14 -0700
commita0ec01668bf62b609d19527a12e88552d6da36f4 (patch)
tree0d212e0dc4432e27c3cb6a43258469afb34e17c2 /doc
parent8ff642d41304854bbe3703503d6dbae562b467bb (diff)
Add the options figure
Diffstat (limited to 'doc')
-rw-r--r--doc/manual_src/figures/options.pngbin0 -> 52606 bytes
1 files changed, 0 insertions, 0 deletions
diff --git a/doc/manual_src/figures/options.png b/doc/manual_src/figures/options.png
new file mode 100644
index 0000000..4305a02
--- /dev/null
+++ b/doc/manual_src/figures/options.png
Binary files differ