add php 7.1

diff --git a/PLD_Builder/request.py b/PLD_Builder/request.py
index eba63fc248e247644ee3ac55f23b84f9b2e9ee22..24784c062298edb749c87cab1c6d7f0a889ce09f 100644 (file)
--- a/PLD_Builder/request.py
+++ b/PLD_Builder/request.py
@@ -407,7 +407,7 @@ class Batch:
             return v.replace('.', '')
 
         # available php versions in distro
-        php_versions = ['4', '5.2', '5.3', '5.4', '5.5', '5.6', '7.0']
+        php_versions = ['4', '5.2', '5.3', '5.4', '5.5', '5.6', '7.0', '7.1']
 
         # current version if -D php_suffix is present
         php_version = php_name_to_ver(self.defines['php_suffix'])