How to define GPIO pin as PPS source device

Question

I'm using Linux in an embedded environment. I want to use a particular GPIO pin as a PPS source to be used with gpsd. I think the pin is configured correctly because I can see high/low transitions using

cat /sys/class/gpio/gpio372/value

I have also defined the GPIO pin as a PPS source in the device tree.

/ {
chosen {
    bootargs = "console=ttyPS0,115200 earlyprintk uio_pdrv_genirq.of_id=generic-uio root=/dev/mmcblk0p2 rw rootwait rootfstype=ext4";
};

pps-gpio {
    compatible = "pps-gpio";
    gpios = <&gpio 372 GPIO_ACTIVE_HIGH>;
    echo-gpios = <&gpio 372 GPIO_ACTIVE_HIGH>;
    echo-active-ms = <100>;
};};

Usually you would tell gpsd to use /dev/pps0, but I am not sure how to assign the GPIO to a device under /dev or how else to configure it.