make php.sh

#!/bin/bash

function make_php_ini() {
  continue_after 5 "Config ini" && return

  if [[ -n "$DEFAULT_INI" ]]; then
    if [[ -f "$PREFIX/$DEFAULT_INI" ]]; then
      cp "$PREFIX/$DEFAULT_INI" "$PREFIX/etc/php.ini"
    else
      if [[ -f "$DEFAULT_INI" ]]; then
        cp "$DEFAULT_INI" "$PREFIX/etc/php.ini"
      fi
    fi
  fi
  log "Config ini" "appending add-on extention configuration to php.ini"
  cat "$PHPENV_ROOT/etc/ext"/* >> "$PREFIX/etc/php.ini"
}