Skip to content

Rename stubs from *.php to *.phpstub#64

Merged
muglug merged 1 commit intopsalm:masterfrom
weirdan:rename-stubs
Apr 5, 2020
Merged

Rename stubs from *.php to *.phpstub#64
muglug merged 1 commit intopsalm:masterfrom
weirdan:rename-stubs

Conversation

@weirdan
Copy link
Copy Markdown
Member

@weirdan weirdan commented Apr 5, 2020

This hides them from PHPStorm, preventing false positives it used to emit.

This hides them from PHPStorm, preventing false positives it used to
emit.
@weirdan
Copy link
Copy Markdown
Member Author

weirdan commented Apr 5, 2020

@radarlog please see if this fixes your PHPStorm issues. I think it's safer approach, compared to #63

@muglug muglug merged commit 4b662fd into psalm:master Apr 5, 2020
@radarlog
Copy link
Copy Markdown
Contributor

radarlog commented Apr 5, 2020

yes, it works. thanks.

then I'm going to close #63

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants