Skip to content

indexing: use String.remove_prefix#1455

Merged
fblanqui merged 1 commit into
Deducteam:masterfrom
fblanqui:prefix
Jul 10, 2026
Merged

indexing: use String.remove_prefix#1455
fblanqui merged 1 commit into
Deducteam:masterfrom
fblanqui:prefix

Conversation

@fblanqui

@fblanqui fblanqui commented Jul 10, 2026 •
edited
Loading

Copy link
Copy Markdown
Member
  • error.ml: fix comment
  • Indexing.parse_file: test prefix "file://" instead of "file:///", and use Lplib.String.remove_prefix
  • Library.path_of_file error message: put filename between double quotes

@fblanqui fblanqui mentioned this pull request Jul 10, 2026
Open
@fblanqui fblanqui merged commit 8a02c23 into Deducteam:master Jul 10, 2026
24 checks passed
@fblanqui fblanqui deleted the prefix branch July 10, 2026 14:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@fblanqui