Merge pull request #696 from agda/Saizan-patch-1

Do not ask users to run `make` to install the library.
agda · Mar 15, 2022 · d8edbe5 · d8edbe5
2 parents fcb160e + fd06135
commit d8edbe5
Showing 1 changed file with 3 additions and 6 deletions.
diff --git a/INSTALL.md b/INSTALL.md
@@ -83,10 +83,9 @@ Once this works go to a suitable directory and run
 ```
 > git clone https://github.com/agda/cubical
 > cd cubical
-> make
 ```
 
-This should compile all of the agda/cubical files. To test that it
+You can additionally run `make` to typecheck all of the agda/cubical files, otherwise they will be checked as needed. To test that it
 works in emacs run
 
 ```
@@ -164,10 +163,9 @@ Once this works go to a suitable directory and run
 ```
 > git clone https://github.com/agda/cubical
 > cd cubical
-> make
 ```
 
-This should compile all of the agda/cubical files. To test that it
+You can additionally run `make` to typecheck all of the agda/cubical files, otherwise they will be checked as needed. To test that it
 works in emacs run
 
 ```
@@ -248,10 +246,9 @@ Once this works go to a suitable directory and run
 ```
 > git clone https://github.com/agda/cubical
 > cd cubical
-> make
 ```
 
-This should compile all of the agda/cubical files. To test that it
+You can additionally run `make` to typecheck all of the agda/cubical files, otherwise they will be checked as needed. To test that it
 works in emacs run
 
 ```