-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA256 > >>> +lib/ocaml/coq/doc/ > >>> +lib/ocaml/coq/doc/tools/ > >>> +lib/ocaml/coq/doc/tools/docgram/ > > > > docgram directory is empty. > > it should be removed? or put README.md and other files here?
aha, docgram files are for generating documentation, and we don't need them for packaging. they should be commented out in PLIST. it is used only when we add option "-with-doc yes" for configure and documentation is generated. (/coq-8.11.2/doc/tools/docgram/README.md) > # Grammar extraction tool for documentation > > `doc_grammar` extracts Coq's grammar from `.mlg` files, edits it and inserts > it in > chunks into `.rst` files. The tool currently inserts Sphinx > `productionlist` constructs. It also generates a file with `prodn` constructs ........ -- yozo. -----BEGIN PGP SIGNATURE----- iQJJBAEBCAAzFiEEP48DGKttLBTWuiCMx2ep6SZGbGQFAl8JjGgVHHlvem9AdjAw Ny52YWlvLm5lLmpwAAoJEMdnqekmRmxksqAP/jdwaFBncktiqGTSeOgFlYFYSZmg J7F4gRtXT9mHMMcFE4aUVfVz6zzGY1Uxv3bDlqeZxTtRjhZpSJiZeXUFlqbLvY6L nJwNdDMr/m3rwFng0EaY68o3zH8/Xwn+58HSWShBsF+Z4l0MhBtPmcKPP+dVsG/j Hp1arXBuim+JjzocKTP3fC/AIuCoJpUBVhKI5GSPej0F0Fs3BVKa8zUWirmSkkVY h0jHNZ/tAjZZlZrlH2SbbGZNNIabqV6CYC978iS7Kfa/K7LGKIY/qhYsHP6YfsQw 2vrf9DQVWaekvnLsFU/qTLsSelDxosssjEh8a3N2dxSWETVi8xWJNyu28/7QKhEO g7rrSbobGstWD5Z6oPWErDFmHM5Uz7pXagWKZlrAa39hsuzPG1IXSuDOFJL8+rFR 40kdhpHI3DAw8mD/k5A+Dv0Em9C54IlyQwEUMUXVFsAj/mSNP5atTwE50ksv0qf8 EYH7nzs5IGaNiwcheNt5dcQMQohnqLQbgmPueGXjSZuOHmms0gc3+iOMKuUdC4Wr UtPNSZvOP2I3RCudoPk4dvzPNW2JOkLI1ToborLoGQIF11tGbdu+45DCrtVXzsNj Qz9QiMA3Ggw2bpXxn9um31meDSmJ06FjxYPnk3LdQ9sSoYz9dBPeG/PMZ7c5OfQd NLlFRngP2w7pis37 =xwvV -----END PGP SIGNATURE-----
