Merge branch 'micro' into maint

Merge branch 'micro' into maint

* micro:
  tests: avoid a couple of extra sleep with GNU make
  NEWS: document testsuite work for 1.13.3
  lint: remove a couple of obsolete syntax checks
  lint: cosmetics: use #-comments, not ##-comments
  lint: cosmetics: some reordering
  lint: recipes of syntax check require GNU grep; ensure it is used
  lint: better name for a syntax check
  tests: rename $am_make_rc_got -> $am_make_rc
  tests: ensure $required is not set too late

Signed-off-by: Stefano Lattarini <stefano.lattarini@gmail.com>