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?
to your account
The HistoryKey curently distinguishes between pathes which are empty ('') or null. Since they are semantically the same they should be treated the same.
The text was updated successfully, but these errors were encountered:
I will take it up.
Sorry that I took three months to deliver send this pull request. My bad!
However, is it possible to configure (some xml file?) history related information during the startup time?
Reviewed PR #233 and added to changes.ml
This PR fixes #150 and fixes #221.
Successfully merging a pull request may close this issue.