Skip to content

Conversation

@kroening
Copy link
Collaborator

When adding "file.txt" to "some/path/" there is no need to add
another '/'.

This is a cosmetical change, for the benefit of user-facing output, since
both Unix-like OSs and Windows tolerate the additional directory separators.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

When adding "file.txt" to "some/path/" there is no need to add
another '/'.

This is a cosmetical change, for the benefit of user-facing output, since
both Unix-like OSs and Windows tolerate the additional directory separators.
@kroening kroening marked this pull request as ready for review March 16, 2020 11:25
@kroening kroening merged commit c532502 into develop Mar 18, 2020
@kroening kroening deleted the concat-dir-file branch March 18, 2020 10:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants