I pushed two days ago, but the manual hasn't updated yet. I guess it doesn't update on git hooks like worg. is there a scheduled process or is there something that must be done?
On Thu, Nov 5, 2020 at 11:03 PM Kyle Meyer <[email protected]> wrote: > ian martins writes: > > > Subject: [PATCH] org-manual.org: Remove language list and fix Worg link > > > > * doc/org-manual.org: Remove the language list and fix the Worg link > > since the languages page has moved. Renumber footnotes. > > > > The language list in the manual is missing many languages. Rather > > than trying to keep the list up to date in two places that link to > > each other, this removes the list from the manual which is updated > > less frequently. There were a few footnotes in the table, so this > > also renumbers the remaining footnotes. > > Sounds like a good idea to me. > > > The languages page was moved in Worg to make it the index page in the > > languages directory. This updates the link in the manual to point to > > its new location. > > --- > > doc/org-manual.org | 103 +++++++++++++++++---------------------------- > > 1 file changed, 38 insertions(+), 65 deletions(-) > [...] > > -[fn:160] Note that, for ~org-odd-levels-only~, a level number > > +[fn:158] Note that, for ~org-odd-levels-only~, a level number > > corresponds to order in the hierarchy, not to the number of stars. > > > > [fn:161] If you move entries or Org files from one directory to > > Hmm, the 158 to 161 jump after your renumbering caught my eye, but it > looks like it's orthogonal to your changes. There was a bad merge > conflict resolution in 9410fbe06 that unlinked this definition from its > reference (one of the two [fn:89]s). I'll clean it up after your > changes land. >
