>
> I disagree that nobody uses it, but if we get rid of ~/.petscrc and
> recommend that they use PETSC_OPTIONS for that, what will they do?
>

I repeat, do we have any data on the number of user that use ~/.petscrc ?

I never have.  That is not data; that is an anecdote.  Data?

If everyone is using ~/.petscrc then I can suck it up but if nobody is then
this is a red hearing and we should just do it.

Reply via email to