]> granicus.if.org Git - php/commit
Remove phpextdist
authorPeter Kokot <peterkokot@gmail.com>
Sat, 4 May 2019 15:57:54 +0000 (17:57 +0200)
committerPeter Kokot <peterkokot@gmail.com>
Sun, 5 May 2019 22:15:20 +0000 (00:15 +0200)
commite58fddf7a3d23b5b7b3cda48c5062ea4c274d5c0
treea1409422cb8125eb4f4c33ec011f2f0e96c4606d
parent340c39acfa165990150b68ac52d11dbdc2003eba
Remove phpextdist

This script hasn't been used since using PEAR as a package manager for
PHP extensions since it is using Makefile.in as an indicator if the
current directory is extension. Instead of this script extensions can
be packaged differently and more properly with either current PEAR
or with some other manual method.
scripts/dev/phpextdist [deleted file]