Closed buzden closed 8 months ago
What is the reason for turning off the max line length in .editorconfig?
What is the reason for turning off the max line length in .editorconfig?
It is turned off only for expected
golden files, because it seems to be useless to require this.
You can see that I added your requirement on the length of 80 to all other files in the top of the editorconfig, but it turned out that most of the files currently do not fulfill this, so I commented it -- either all files should be reformatted in a separate PR, or the requirement should be revised.
I'll merge this, then. Thanks for taking care of this.
I'll merge this, then. Thanks for taking care of this.
Oh, thanks, but it seems I wasn't clear enough -- I planned to sort out dockerfile-related stuff, but I didn't manage to finish this yesterday. Anyway, I'll do a separate PR fixing linter problems with the dockerfile.
This is a technical stuff, originated by deprecation warnings shown by GitHub Actions and breaking changes in the upstream actions behaviour
EDIT: current problems are in liniting of the Dockerfile. Both problems are reasonable, but the first one maybe should be suppressed, since doing things properly will break everyone's usage of the pack's docker image for those who set
PACK_DIR
to/root/.pack
manually.EDIT2: ...but doing things properly will make transition from other's idris-containing images to the pack one seamless, without a need to reser the variable
EDIT3: maybe, we can make a proper user, and just add a symlink of
/root/.pack
to/home/<pack-user>/.pack
for the seamless backwards compatibility. Also, settingPACK_DIR
in the docker file seems to be a good idea, to not to make users to do the same thing again and again.