CI: disable PHP Redis module in phplint call #17

Merged

n merged 1 commit from lint into main 2025-12-10 21:10:55 +01:00

Conversation 0 Commits 1 Files changed 1 +7 -1

n commented 2025-12-10 21:08:41 +01:00

Owner

Copy link

No description provided.

n added 1 commit 2025-12-10 21:08:43 +01:00

CI: disable PHP Redis module in phplint call ee0c74abc1

n merged commit ee0c74abc1 into main 2025-12-10 21:10:55 +01:00

n deleted branch lint 2025-12-10 21:10:58 +01:00

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference

n/shaarli-plugin-shaargem!17

No description provided.