#!/bin/bash

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