Update build-system.txt

(cherry picked from commit 0001b6d)
coq · May 23, 2019 · 82e097e · 82e097e
1 parent 119966b
commit 82e097e
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
@@ -18,8 +18,8 @@ See http://www.gnu.org/software/make/manual/make.htmlPrerequisite-Types
 * Annotation before commands: +/-/@
 
 a command starting by - is always successful (errors are ignored)
-a command starting by + is ran even if option -n is given to make
-a command starting by @ is not echoed before being ran
+a command starting by + is run even if option -n is given to make
+a command starting by @ is not echoed before being run
 
 * Custom functions