php/web-rmtools
1
0
Fork 0
mirror of https://github.com/php/web-rmtools.git synced 2026-03-24 01:02:11 +01:00
Code Issues 12 Packages Projects Releases Wiki Activity

[PR #7] [CLOSED] Disable ext/interbase #14

New Issue
Closed
opened 2026-01-24 11:41:38 +01:00 by admin · 0 comments
admin commented 2026-01-24 11:41:38 +01:00
Owner
Copy Link

📋 Pull Request Information

Original PR: https://github.com/php/web-rmtools/pull/7
Author: @cmb69
Created: 3/25/2019
Status: ❌ Closed

Base: master ← Head: disable-ibase

📝 Commits (1)

📊 Changes

2 files changed (+5 additions, -5 deletions)

View changed files

📝 data/config/branch/x64/phpmaster.ini (+3 -3)
📝 data/config/branch/x86/phpmaster.ini (+2 -2)

📄 Description

Commit bd73607 of php-src[1] broke the ext/ibase build; following Joe's
reasoning[2] we disable the ext/interbase builds (at least for now).

[1] http://git.php.net/?p=php-src.git;a=commit;h=bd73607b9e4811e7caa9d2ff4d227626ffd35dab
[2] https://github.com/php/php-src/pull/3976#issue-263815945

🔄 This issue represents a GitHub Pull Request. It cannot be merged through Gitea due to API limitations.

## 📋 Pull Request Information **Original PR:** https://github.com/php/web-rmtools/pull/7 **Author:** [@cmb69](https://github.com/cmb69) **Created:** 3/25/2019 **Status:** ❌ Closed **Base:** `master` ← **Head:** `disable-ibase` --- ### 📝 Commits (1) - [`d7a27a3`](https://github.com/php/web-rmtools/commit/d7a27a3fe19c8fe5bb1ee966313cd7ed58d8fc55) Disable ext/interbase ### 📊 Changes **2 files changed** (+5 additions, -5 deletions) <details> <summary>View changed files</summary> 📝 `data/config/branch/x64/phpmaster.ini` (+3 -3) 📝 `data/config/branch/x86/phpmaster.ini` (+2 -2) </details> ### 📄 Description Commit bd73607 of php-src[1] broke the ext/ibase build; following Joe's reasoning[2] we disable the ext/interbase builds (at least for now). [1] <http://git.php.net/?p=php-src.git;a=commit;h=bd73607b9e4811e7caa9d2ff4d227626ffd35dab> [2] <https://github.com/php/php-src/pull/3976#issue-263815945> --- <sub>🔄 This issue represents a GitHub Pull Request. It cannot be merged through Gitea due to API limitations.</sub>
admin added the pull-request label 2026-01-24 11:41:38 +01:00
admin closed this issue 2026-01-24 11:41:38 +01:00
Sign in to join this conversation.
No Branch/Tag Specified
Branches Tags
Labels
Clear labels
pull-request
Mirrored from GitHub Pull Request
No Label pull-request
Milestone
No items
No Milestone
Projects
Clear projects
No project
Assignees
Clear assignees
admin
No Assignees
1 Participants
Notifications
Due Date
No due date set.
Dependencies

No dependencies set.

Reference: php/web-rmtools#14
Delete Branch "%!s()"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?