Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use $MAKE if set, otherwise fall back to system specific make command #1036

Merged
merged 4 commits into from
Nov 22, 2024

Conversation

jgabry
Copy link
Member

@jgabry jgabry commented Nov 18, 2024

Submission Checklist

  • Run unit tests
  • Declare copyright holder and agree to license (see below)

Summary

closes #1035

Updates the way we select which make command to use:

Uses Sys.getenv("MAKE") if set otherwise uses current logic of selecting system specific make command.

Copyright and Licensing

Please list the copyright holder for the work you are submitting
(this will be you or your assignee, such as a university or company):
Columbia University

By submitting this pull request, the copyright holder is agreeing to
license the submitted work under the following licenses:

- mingw32-make is no longer required on Windows

closes #1035
@jgabry
Copy link
Member Author

jgabry commented Nov 18, 2024

@WardBrian, mind taking a quick glance at this when you have a chance? (Not particularly urgent if you're busy, since what we have currently should still work.)

@jgabry jgabry changed the title Update selection of make command post CmdStan 2.35 Use $MAKE if set otherwise fall back to system specific default make command Nov 22, 2024
@jgabry jgabry changed the title Use $MAKE if set otherwise fall back to system specific default make command Use $MAKE if set, otherwise fall back to system specific make command Nov 22, 2024
@jgabry
Copy link
Member Author

jgabry commented Nov 22, 2024

The failures, as mentioned in #1035, were due to install_cmdstan() needing make before we could check cmdstan_version(). For now, we'll just default to $MAKE if set and otherwise keep the current logic.

@jgabry jgabry merged commit c681d32 into master Nov 22, 2024
11 checks passed
@jgabry jgabry deleted the update-make-command branch November 22, 2024 18:45
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.

mingw32-make is no longer required on Windows
1 participant