summaryrefslogtreecommitdiff
path: root/README.md
diff options
context:
space:
mode:
Diffstat (limited to 'README.md')
-rw-r--r--README.md2
1 files changed, 1 insertions, 1 deletions
diff --git a/README.md b/README.md
index 6e60657d..e3a7e0e9 100644
--- a/README.md
+++ b/README.md
@@ -75,7 +75,7 @@ If you run `make`, you will generate a documentation accessible from [`doc.html`
## Usage
-The simplest way to run Aeneas is to execute `dune exec -- src/main.exe [OPTIONS] LLBC_FILE`,
+The Aeneas binary is in `bin`; you can run: `./bin/aeneas.exe [OPTIONS] LLBC_FILE`,
where `LLBC_FILE` is an .llbc file generated by Charon.
Aeneas provides a lot of flags and options to tweak its behaviour: you can use `--help`