#!/bin/bash

hvconfig_pre()
{
    CONFIGURE_OPTS="\
        ${CONFIGURE_OPTS} \
        --disable-devel-docs"
}