W3C home > Mailing lists > Public > public-webplatform@w3.org > December 2012

tool for local batch edits

From: Mike Sierra <letmespellitoutforyou@gmail.com>
Date: Thu, 13 Dec 2012 14:43:14 -0500
Message-ID: <CAECD241D9QJEFRS6=PZJ2hBv_7xw5-gOP3JJ+dFLhvcorwLcfQ@mail.gmail.com>
To: public-webplatform@w3.org
I recently used the wpd utility to push locally edited MediaWiki files
to corresponding pages on the server, and found it to be extremely
convenient:
https://github.com/borismus/webplatform-tools

To make things a little easier, I set up a corresponding scraper to
get files from the server, and feel free to use it:
https://github.com/mike-sierra/webplatform/blob/master/src/wpdget.pl

As lightweight traffic control before pushing your edits back, it can
also check if files have been edited in the interim.

For a decent-sized task to test the workflow, I cross-referenced all
the interface & member names in the recently added Web Audio API doc.

BTW, it was unclear in the webplatform API doc how to get the same
markup you can later push back with "edit", hence the crappy scraper.

--Mike Sierra
Received on Thursday, 13 December 2012 19:43:42 UTC

This archive was generated by hypermail 2.3.1 : Wednesday, 8 May 2013 19:57:36 UTC