add php 7.2

diff --git a/PLD_Builder/request.py b/PLD_Builder/request.py
index d66711e6b5a406f6e449c6747f57f5b9b45e2c53..4c47d0661852a8e6d67ae9929bab009c2b8820c4 100644 (file)
--- a/PLD_Builder/request.py
+++ b/PLD_Builder/request.py
@@ -409,7 +409,7 @@ class Batch:
 
     def php_ignores(self, php_version):
         # available php versions in distro
-        php_versions = ['4', '5.2', '5.3', '5.4', '5.5', '5.6', '7.0', '7.1']
+        php_versions = ['4', '5.2', '5.3', '5.4', '5.5', '5.6', '7.0', '7.1', '7.2']
 
         # remove current php version
         try: