[paparazzi-commits] [paparazzi/paparazzi] d57543: [settings] add widget attribute

[GitHub]

  Branch: refs/heads/master
  Home:   https://github.com/paparazzi/paparazzi
  Commit: d575430ddef45db93aaa54ece12c2b7de7d6edc6
      
https://github.com/paparazzi/paparazzi/commit/d575430ddef45db93aaa54ece12c2b7de7d6edc6
  Author: Felix Ruess <address@hidden>
  Date:   2014-08-25 (Mon, 25 Aug 2014)

  Changed paths:
    M conf/settings/settings.dtd
    M sw/ground_segment/cockpit/page_settings.ml

  Log Message:
  -----------
  [settings] add widget attribute

If widget attribute contains one of "radio", "combo", "slider", "spin" that 
widget is used,
otherwise still automatically decides which widget to use.
Not the nicest OCaml code, but works...
Also properly extract number of decimal digits and use that for spin button as 
well.
as requested in #795