<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">Few more comments:<div class=""><br class=""></div><div class=""><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69);" class="">All “$ waf” should be “$ ./waf” (at least on my Gentoo system)</div><div style="margin: 0px; line-height: normal; font-family: Menlo; color: rgb(69, 69, 69);" class=""><span style="line-height: normal; font-family: Helvetica;" class="">“</span>/dev/gpsps0” should be “/dev/gpspps0” (typo in some of the verbiage)</div><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69);" class=""><br class=""></div><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69);" class="">dhcpcd will “merge” DHCP supplied NTP servers at the bottom of a ntp.conf. This has not caused me any issues (on Gentoo). NTP generally does the “right” things and uses all the NTP servers in the config & will decide the local server, with PPS is the best.</div></div><div class=""><br class=""></div></body></html>