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

Fix unused variable warnings. #5760

Merged
merged 1 commit into from
Jan 9, 2022
Merged

Fix unused variable warnings. #5760

merged 1 commit into from
Jan 9, 2022

Conversation

nadavrot
Copy link
Contributor

@nadavrot nadavrot commented Jan 8, 2022

This commit fixes a few cases of unused variables in release builds.
The commit uses the (void)xxx; syntax which is used in other parts of
the code.

This commit fixes a few cases of unused variables in release builds.
The commit uses the (void)xxx; syntax which is used in other parts of
the code.
@ghost
Copy link

ghost commented Jan 8, 2022

CLA assistant check
All CLA requirements met.

@NikolajBjorner NikolajBjorner merged commit 9f9543e into Z3Prover:master Jan 9, 2022
@nunoplopes
Copy link
Collaborator

Welcome Nadav! 🤗

@NikolajBjorner
Copy link
Contributor

@nunoplopes - since you have time to read pull requests, can I assign some issues to you?

@nunoplopes
Copy link
Collaborator

@nunoplopes - since you have time to read pull requests, can I assign some issues to you?

ahah, sure as long as you write my grant proposals 😅

@NikolajBjorner
Copy link
Contributor

the excuse doesn't work: you still had too much time to spend on reading github activity.

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