search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
491 stars 88 forks source link

Change _CoqProject separator settings #784

Closed Columbus240 closed 2 months ago

Columbus240 commented 3 months ago

According to the code of coq_makefile, ~\r is not considered white-space in _CoqProject. But \t is.~ \t is considered white-space. Source: https://github.com/coq/coq/blob/a7f51315db5d70888af3b96a579eb799a2b45ca9/lib/coqProject_file.ml#L84

The second commit of this PR removes a duplicate function definition.

SkySkimmer commented 3 months ago

\r seems to be treated the same as \t and in that code?

Columbus240 commented 3 months ago

Oh! I'm sorry for the mistake. Maybe just add \t then?