Update build-system.txt

coq · May 21, 2019 · 0001b6d · 0001b6d
1 parent e6322e2
commit 0001b6d
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