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

Extend statistics use in the local search planner #146

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from

Conversation

ujhelyiz
Copy link
Contributor

This PR was initialized from the Gerrit change https://git.eclipse.org/r/c/viatra/org.eclipse.viatra/+/129938 and should be related to ticket #89 in Github.

Given it required non-trivial merges, I have not rebased it over current master, @bergmanngabor please ensure if there is something on Gerrit related this PR that is important to kept indefinitely please copy it to this PR.

Change-Id: I313b3623b2e11d42a758f4d5790f9faba1b3b70f
Task-Url: https://bugs.eclipse.org/bugs/show_bug.cgi?id=538742
Signed-off-by: bergmann <bergmann@mit.bme.hu>
Change-Id: Ia8ef06380399ffa4dd896f08c5051cc6acd1c356
Task-Url: https://bugs.eclipse.org/bugs/show_bug.cgi?id=538742
Signed-off-by: bergmann <bergmann@mit.bme.hu>
@ujhelyiz ujhelyiz removed the legacy label Mar 25, 2024
@ujhelyiz ujhelyiz marked this pull request as draft August 9, 2024 14:58
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.

2 participants