diff options
| author | Jakob Unterwurzacher | 2017-11-01 20:05:15 +0100 |
|---|---|---|
| committer | Jakob Unterwurzacher | 2017-11-01 20:05:15 +0100 |
| commit | 843138168ff381b81fb0774cdb563937d9fff7a1 (patch) | |
| tree | a34981f5a5f263c1f586002cddb870bb8ca1179f /profiling | |
| parent | 5428567fa09019cb844c59700d7ffc2a49719f51 (diff) | |
package-source.bash: replace plus sign in file name
Plus signs are apparently not supported on github,
and replaced by a dot.
Diffstat (limited to 'profiling')
0 files changed, 0 insertions, 0 deletions