Is the diff_manual.sh used any more?

Developers
1

We have a script sitting at the top level of the Stan repo (stan-dev/stan) called diff_manual.sh. Is it used any more?
https://github.com/stan-dev/stan/blob/develop/diff_manual.sh

If not, I’ll create an issue to remove. If it is, can we move it under src/doc?

2

I haven’t run it for like 5 releases. No one was uploading the diffed manual anywhere.

3

Ok. I’ll create an issue to remove it.

4

Not that I know of. This is probably all going to be moot
soon when we move the manual to some kind of online doc.

  • Bob