diff options
-rw-r--r-- | profiles/server/make.defaults | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/profiles/server/make.defaults b/profiles/server/make.defaults index 69a83fe4..7d56cfec 100644 --- a/profiles/server/make.defaults +++ b/profiles/server/make.defaults @@ -772,9 +772,10 @@ USE="${USE} -php_targets_php7-0 -php_targets_php7-1 -php_targets_php7-2 - -php_targets_php7-3" + -php_targets_php7-3 + -php_targets_php7-4" USE="${USE} - php_targets_php7-3" + php_targets_php7-4" # 25/08/2019 - beber # Setting GRUB_PLATFORMS is non functional, need to expand manually |