From dc9b11c33d0f3283b82f2c87bfd7dd4c7126b0d0 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Mon, 27 Apr 2020 13:42:28 -0700
Subject: Fix examples instructions in INSTALL.md. (#4397)

---
 INSTALL.md | 30 +-----------------------------
 1 file changed, 1 insertion(+), 29 deletions(-)

(limited to 'INSTALL.md')

diff --git a/INSTALL.md b/INSTALL.md
index 17d31fe1a..9fc2b52c1 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -203,17 +203,7 @@ binding, please contact one of the project leaders.
 
 ## Building the Examples
 
-The examples provided in directory `examples` are not built by default.
-
-    make examples                      # build all examples
-    make runexamples                   # build and run all examples
-    make <example>                     # build examples/<subdir>/<example>.<ext>
-    ctest example/<subdir>/<example>   # run test example/<subdir>/<example>
-
-All examples binaries are built into `<build_dir>/bin/examples`.
-
-See `examples/README` for more detailed information on what to find in the
-`examples` directory.
+See `examples/README.md` for instructions on how to build and run the examples.
 
 ## Testing CVC4
 
@@ -238,24 +228,6 @@ We have 4 categories of tests:
 - **unit tests** in directory `test/unit`
   (label: **unit**)
 
-### Testing Examples
-
-For building instructions, see [Building the Examples](building-the-examples).
-
-We use prefix `example/` + `<subdir>/` + `<example>` (for `<example>` in
-`example/<subdir>/`) as test target name.  
-
-    make bitvectors                       # build example/api/bitvectors.cpp
-    ctest -R bitvectors                   # run all tests that match '*bitvectors*'
-                                          # > runs example/api/bitvectors
-                                          # >      example/api/bitvectors_and_arrays
-                                          # >      ...
-    ctest -R bitvectors$                  # run all tests that match '*bitvectors'
-                                          # > runs example/api/bitvectors
-    ctest -R example/api/bitvectors$      # run all tests that match '*example/api/bitvectors'
-                                          # > runs example/api/bitvectors
-
-
 ### Testing System Tests
 
 The system tests are not built by default.
-- 
cgit v1.2.3