<?php

/**
 * Part of .inc migration to .inc.php to better support source code editors.
 *  - registry.inc stub that redirects to registry.inc.php
 *  - Timeframe: this script can be remove in mid 2023
 */

require_once(dirname(__FILE__) . "/registry.inc.php");