Make etags.sh executable
XDOC support for KaTeX, and supporting updates

 - XDOC now supports LaTeX-like formulas within new @([...]) and @($...$)
   directives.  This is experimental.  See XDOC::KATEX-INTEGRATION for details.
   I would greatly appreciate any reports of web-browser incompatibilities
   related to this feature (or other xdoc features, for that matter).

 - OSLIB has been reorganized somewhat to try to make it more coherent.  Many
   files in oslib are now split up into, e.g., argv-logic.lisp (no raw code or
   ttags) and argv.lisp (actual implementation).

 - OSLIB has new functions for getting the dirname/basename from a path.
   These may be somewhat buggy since Lisp pathname stuff is awful.  See
   OSLIB::BASENAME and OSLIB::DIRNAME.

 - OSLIB has new functions for copying files and directories, See OSLIB::COPY.

 - Slightly extended Quicklisp directory with UIOP library and a more sensible
   CL-FAD book, in support of the above OSLIB changes.

 - XDOC::SAVE now uses OSLIB::COPY to copy the entire xdoc/fancy directory
   into the new manual.  (This avoids big ugly lists of files in the xdoc
   source code.)

 - Documented new #{"""..."""} string literal syntax, see
   ACL2::FANCY-STRING-READER.
Fixes for getopt demo2.

Give up on the goal of suppressing Lisp banners by tweaking the getopt test
script to permit other text before the expected output.  Also tweaked
OSLIB::ARGV to accommodate the new handling of "--" in GCL.  This simplifies
the GNUmakefile by avoiding some Lisp-specific mechanisms.

I think this fixes #210 and fixes #211.  There is some chance that it might
also resolve issue 213, but I don't have a convenient way to run Lispworks and
Allegro so I haven't tried to investigate.

Patched acl2-bridge to avoid hl-hspace-init unless #+hons.  I think this
resolves #229.
4v-sexpr: fill out the sexpr-rewrites a bit more
Rager merge remote-tracking branch 'remotes/origin/master' into make-chmod
Fty::deftypes: Allow deflist/defalist with already-defined predicates
VL: fix bonehead scopestack performance bug; improve certification time of a couple critical books
Initial fix-up of google code references
Merge changes from acl2 community repo into ragerdl repo.
Changing my email address in the quickstart and making a wiki page reference slightly more canonical (it's actually case-insensitive, but the filename is sentence case).
XDOC fancy viewer updates and bugfixes

 - Ported xdoc fancy viewer to newer versions of jquery and typeahead

 - Fixed up typeahead box (jump to box) to be less horrible, showing
   many more results with a scroll-bar if necesary, and adding "return
   key chooses first item" support.  I think I'll claim this fixes #149.

 - (with Sol) make middle click work in xdoc.  Senseless hacking.  Seems to
   work in Chrome and Firefox.  Fixes #148.

Please report any portability issues...
Brought doc.lisp up to date with books/system/doc/acl2-doc.lisp.
Merge remote-tracking branch 'remotes/origin/master'
Avoid certifying oslib/tests/dirname on Allegro and Lispworks

 - Added new 'non-allegro' and 'non-lispworks' cert params.
 - Extended Makefile to exclude these books as appropriate.

Haven't really tested this, but I think it should work.
Made theory functions tail recursive in books/ihs/ihs-theories.lisp.  Changed license on books/data-structures/array1.lisp to 3-clause BSD,

Changed some theories in books/ihs/ihs-theories.lisp to be
tail-recursive, to avoid memory growing too large for ACL2(h) built on
Allegro CL.

Changed license on books/data-structures/array1.lisp to 3-clause BSD,
as arranged with copyright holder (apparently an oversight that this
didn't happen sooner; thanks to Jared Davis for pointing this out).
add support for non-sbcl cert-param, add non-allegro cert-param to oslib/file-types
Merge pull request #241 from ragerdl/master

Fixup googlecode references
Tweak to avoid building Quicklisp on GCL
avoid dirname tests on sbcl also
Adding reference to books/std/std-customization.lsp from :doc topic working-with-packages.