Skip to content

fail directly when lean --print-libdir returns no output#534

Merged
cdisselkoen merged 4 commits intomainfrom
cdisselkoen/tweak-script
Feb 10, 2025
Merged

fail directly when lean --print-libdir returns no output#534
cdisselkoen merged 4 commits intomainfrom
cdisselkoen/tweak-script

Conversation

@cdisselkoen
Copy link
Contributor

Test for the case where lean --print-libdir returns no output, and fail directly if so. Currently, we instead set LD_PRELOAD to /lib/glibc/libm.so which is unlikely to exist, which causes more confusing errors.

Signed-off-by: Craig Disselkoen <cdiss@amazon.com>
Signed-off-by: Craig Disselkoen <cdiss@amazon.com>
cdisselkoen and others added 2 commits February 10, 2025 10:54
Signed-off-by: Craig Disselkoen <cdiss@amazon.com>

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Signed-off-by: Craig Disselkoen <cdiss@amazon.com>
@cdisselkoen cdisselkoen merged commit db9e8ec into main Feb 10, 2025
6 checks passed
@cdisselkoen cdisselkoen deleted the cdisselkoen/tweak-script branch February 10, 2025 16:16
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