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.

Sign up for GitHub

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

Jump to bottom

Make profiling correctly handle the same file being opened multiple times #1069

Merged
merged 1 commit into from
Jan 13, 2017
Merged

Make profiling correctly handle the same file being opened multiple times #1069

merged 1 commit into from
Jan 13, 2017

Commits on Jan 13, 2017

  1. Make profiling correctly handle opening the same file multiple times 

    This patch ensures when reopening a file we check if the filename
has been opened previously, and if so associate it with the same
filename number.

This is tested in the 'profiling' package, which is why there is no
tests here.
    @ChrisJefferson
    ChrisJefferson committed Jan 13, 2017
    Configuration menu
    Copy the full SHA
    bc95e8b View commit details
    Browse the repository at this point in the history