On my Mac system, the presence of two files which have an identical name up to capitalization is causing a problem where git overwrites one with another. (It warned about this when I first cloned the repo.) Could the peps.jl file be renamed to something distinct, such as peps_util.jl or similar?
On my Mac system, the presence of two files which have an identical name up to capitalization is causing a problem where git overwrites one with another. (It warned about this when I first cloned the repo.) Could the peps.jl file be renamed to something distinct, such as peps_util.jl or similar?