Changes in configure [4ec769c:4149d9d]

File:

• configure (modified) (2 diffs)

configure

@@ -6281 +6281 @@
 
 
-ac_config_files="$ac_config_files Makefile src/driver/Makefile src/Makefile src/benchmark/Makefile src/examples/Makefile src/tests/Makefile src/tests/preempt_longrun/Makefile src/prelude/Makefile src/libcfa/Makefile tools/prettyprinter/Makefile"
+ac_config_files="$ac_config_files Makefile src/driver/Makefile src/Makefile src/benchmark/Makefile src/examples/Makefile src/tests/Makefile src/tests/preempt_longrun/Makefile src/prelude/Makefile src/libcfa/Makefile tools/Makefile tools/prettyprinter/Makefile"
 
 
@@ -7048 +7048 @@
     "src/prelude/Makefile") CONFIG_FILES="$CONFIG_FILES src/prelude/Makefile" ;;
     "src/libcfa/Makefile") CONFIG_FILES="$CONFIG_FILES src/libcfa/Makefile" ;;
+    "tools/Makefile") CONFIG_FILES="$CONFIG_FILES tools/Makefile" ;;
     "tools/prettyprinter/Makefile") CONFIG_FILES="$CONFIG_FILES tools/prettyprinter/Makefile" ;;