From 0524c2524919ccfaa8f05f3ef72ae5aecae88377 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Fri, 7 Jan 2022 11:53:06 +0100
Subject: [PATCH] README.

---
 benchmark/README.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/benchmark/README.md b/benchmark/README.md
index f22f04f..a67ec99 100644
--- a/benchmark/README.md
+++ b/benchmark/README.md
@@ -89,6 +89,11 @@ To view the most-recently-generated `.pdf` file, just type:
   make view
 ```
 
+## A shortcut
+
+The command `./make.sh bench <benchmark>` is a shortcut for
+`./make.sh run <benchmark> && ./make.sh plot <benchmark> && ./make.sh view`.
+
 ## Comparing several runs
 
 To compare several runs, proceed as in this example:
-- 
GitLab