diff --git a/configure b/configure index 8840027d640a60f5945bc140bf27f2de084d1bab..5913090f7eab9a21aa72431376a7c70cf1784d8b 100755 --- a/configure +++ b/configure @@ -5958,6 +5958,10 @@ test -n "$random_seed" && echo "random seed ${random_seed}" echo +echo "Enabled programs:" +print_enabled '' $PROGRAM_LIST | print_3_columns +echo + echo "External libraries:" print_enabled '' $EXTERNAL_LIBRARY_LIST | print_3_columns echo