rc.d/ntpdate broken since r311103 - /head/etc/ntp.conf - Update ntp.conf to use the ntpd pool feature

Hello,

Since the commit in the subject /etc/rc.d/ntpdate does not work anymore.
# /etc/rc.d/ntpdate restart
Setting date via ntp.
11 Jan 00:35:46 ntpdate[56020]: no servers can be used, exiting

This diff fixes it for me:
# diff -u /tmp/ntpdate /etc/rc.d/ntpdate
--- /tmp/ntpdate	2017-01-11 00:41:58.736138000 +0100
+++ /etc/rc.d/ntpdate	2017-01-11 00:42:15.522986000 +0100
_at__at_ -20,7 +20,7 _at__at_
  	if [ -z "$ntpdate_hosts" -a -f "$ntpdate_config" ]; then
  		ntpdate_hosts=`awk '
  			/^server[ \t]*127.127/      {next}
-			/^(server|peer)/            {
+			/^(server|peer|pool)/            {
  			    if ($2 ~/^-/)           {print $3}
  			    else                    {print $2}}
  		' < "$ntpdate_config"`


Regards,

Ronald.