I have wanted to keep out of this rather fraught discussion, but I agree on this issue. How dangerous it is depends on how critical those secrets are. And I’m perfectly aware that key management can be difficult and maybe there is little point if only one instance of this thing is running. Still, it isn’t ideal.
Larry > On 6 Oct 2016, at 13:00, Makarius <makar...@sketis.net> wrote: > > Putting secrets into a repository is a bad idea -- they stay there > forever, even if they are "deleted" in some versions. When it is clone > eventually, secrets will leak. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
